`∀[X:Type]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)].  ((f+g) = (g+f) ∈ PowerSeries(X;r))`

Proof

Definitions occuring in Statement :  fps-add: `(f+g)` power-series: `PowerSeries(X;r)` uall: `∀[x:A]. B[x]` universe: `Type` equal: `s = t ∈ T` crng: `CRng`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` crng: `CRng` comm: `Comm(T;op)` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` all: `∀x:A. B[x]` fps-add: `(f+g)` fps-coeff: `f[b]` power-series: `PowerSeries(X;r)` infix_ap: `x f y`
Lemmas referenced :  rng_plus_comm fps-ext fps-add_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis productElimination independent_isectElimination lambdaFormation sqequalRule applyEquality because_Cache isect_memberEquality axiomEquality

Latex:
\mforall{}[X:Type].  \mforall{}[r:CRng].  \mforall{}[f,g:PowerSeries(X;r)].    ((f+g)  =  (g+f))

Date html generated: 2016_05_15-PM-09_47_51
Last ObjectModification: 2015_12_27-PM-04_40_47

Theory : power!series

Home Index