let X be RealUnitarySpace; :: thesis: for seq, seq1 being sequence of X st ( for n being Nat holds seq1 . n = seq . 0 ) holds
Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1
let seq, seq1 be sequence of X; :: thesis: ( ( for n being Nat holds seq1 . n = seq . 0 ) implies Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 )
assume A1: for n being Nat holds seq1 . n = seq . 0 ; :: thesis: Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1

A2: now :: thesis: for n being Nat holds (((Partial_Sums seq) ^\ 1) - seq1) . (n + 1) = ((((Partial_Sums seq) ^\ 1) - seq1) . n) + ((seq ^\ 1) . (n + 1))

let n be Nat; :: thesis: (((Partial_Sums seq) ^\ 1) - seq1) . (n + 1) = ((((Partial_Sums seq) ^\ 1) - seq1) . n) + ((seq ^\ 1) . (n + 1))
thus (((Partial_Sums seq) ^\ 1) - seq1) . (n + 1) = (((Partial_Sums seq) ^\ 1) . (n + 1)) - (seq1 . (n + 1)) by NORMSP_1:def 3
.= (((Partial_Sums seq) ^\ 1) . (n + 1)) - (seq . 0) by A1
.= ((Partial_Sums seq) . ((n + 1) + 1)) - (seq . 0) by NAT_1:def 3
.= ((seq . ((n + 1) + 1)) + ((Partial_Sums seq) . (n + 1))) - (seq . 0) by Def1
.= ((seq . ((n + 1) + 1)) + ((Partial_Sums seq) . (n + 1))) - (seq1 . n) by A1
.= (seq . ((n + 1) + 1)) + (((Partial_Sums seq) . (n + 1)) - (seq1 . n)) by RLVECT_1:def 3
.= (seq . ((n + 1) + 1)) + ((((Partial_Sums seq) ^\ 1) . n) - (seq1 . n)) by NAT_1:def 3
.= (seq . ((n + 1) + 1)) + ((((Partial_Sums seq) ^\ 1) - seq1) . n) by NORMSP_1:def 3
.= ((((Partial_Sums seq) ^\ 1) - seq1) . n) + ((seq ^\ 1) . (n + 1)) by NAT_1:def 3 ; :: thesis: verum

end;

(((Partial_Sums seq) ^\ 1) - seq1) . 0 = (((Partial_Sums seq) ^\ 1) . 0) - (seq1 . 0) by NORMSP_1:def 3
.= (((Partial_Sums seq) ^\ 1) . 0) - (seq . 0) by A1
.= ((Partial_Sums seq) . (0 + 1)) - (seq . 0) by NAT_1:def 3
.= (((Partial_Sums seq) . 0) + (seq . (0 + 1))) - (seq . 0) by Def1
.= ((seq . (0 + 1)) + (seq . 0)) - (seq . 0) by Def1
.= (seq . (0 + 1)) + ((seq . 0) - (seq . 0)) by RLVECT_1:def 3
.= (seq . (0 + 1)) + H₁(X) by RLVECT_1:15
.= seq . (0 + 1)
.= (seq ^\ 1) . 0 by NAT_1:def 3 ;
hence Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 by A2, Def1; :: thesis: verum