let X be non empty complex-membered add-closed set ; :: thesis: for s1, s2 being sequence of X holds (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2)

let s1, s2 be sequence of X; :: thesis: (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2)

.= (s1 . 0) + ((Partial_Sums s2) . 0) by Def1

.= (s1 . 0) + (s2 . 0) by Def1

.= (s1 + s2) . 0 by Lm1 ;

hence (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2) by A1, Def1; :: thesis: verum

let s1, s2 be sequence of X; :: thesis: (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2)

A1: now :: thesis: for n being Nat holds ((Partial_Sums s1) + (Partial_Sums s2)) . (n + 1) = (((Partial_Sums s1) + (Partial_Sums s2)) . n) + ((s1 + s2) . (n + 1))

((Partial_Sums s1) + (Partial_Sums s2)) . 0 =
((Partial_Sums s1) . 0) + ((Partial_Sums s2) . 0)
by Lm1
let n be Nat; :: thesis: ((Partial_Sums s1) + (Partial_Sums s2)) . (n + 1) = (((Partial_Sums s1) + (Partial_Sums s2)) . n) + ((s1 + s2) . (n + 1))

thus ((Partial_Sums s1) + (Partial_Sums s2)) . (n + 1) = ((Partial_Sums s1) . (n + 1)) + ((Partial_Sums s2) . (n + 1)) by Lm1

.= (((Partial_Sums s1) . n) + (s1 . (n + 1))) + ((Partial_Sums s2) . (n + 1)) by Def1

.= (((Partial_Sums s1) . n) + (s1 . (n + 1))) + ((s2 . (n + 1)) + ((Partial_Sums s2) . n)) by Def1

.= (((Partial_Sums s1) . n) + ((s1 . (n + 1)) + (s2 . (n + 1)))) + ((Partial_Sums s2) . n)

.= (((Partial_Sums s1) . n) + ((s1 + s2) . (n + 1))) + ((Partial_Sums s2) . n) by Lm1

.= (((Partial_Sums s1) . n) + ((Partial_Sums s2) . n)) + ((s1 + s2) . (n + 1))

.= (((Partial_Sums s1) + (Partial_Sums s2)) . n) + ((s1 + s2) . (n + 1)) by Lm1 ; :: thesis: verum

end;thus ((Partial_Sums s1) + (Partial_Sums s2)) . (n + 1) = ((Partial_Sums s1) . (n + 1)) + ((Partial_Sums s2) . (n + 1)) by Lm1

.= (((Partial_Sums s1) . n) + (s1 . (n + 1))) + ((Partial_Sums s2) . (n + 1)) by Def1

.= (((Partial_Sums s1) . n) + (s1 . (n + 1))) + ((s2 . (n + 1)) + ((Partial_Sums s2) . n)) by Def1

.= (((Partial_Sums s1) . n) + ((s1 . (n + 1)) + (s2 . (n + 1)))) + ((Partial_Sums s2) . n)

.= (((Partial_Sums s1) . n) + ((s1 + s2) . (n + 1))) + ((Partial_Sums s2) . n) by Lm1

.= (((Partial_Sums s1) . n) + ((Partial_Sums s2) . n)) + ((s1 + s2) . (n + 1))

.= (((Partial_Sums s1) + (Partial_Sums s2)) . n) + ((s1 + s2) . (n + 1)) by Lm1 ; :: thesis: verum

.= (s1 . 0) + ((Partial_Sums s2) . 0) by Def1

.= (s1 . 0) + (s2 . 0) by Def1

.= (s1 + s2) . 0 by Lm1 ;

hence (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2) by A1, Def1; :: thesis: verum