let X be ComplexUnitarySpace; :: thesis: for seq1, seq being sequence of X st ( for n being Element of NAT holds seq1 . n = seq . 0 ) holds
Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1
let seq1, seq be sequence of X; :: thesis: ( ( for n being Element of NAT holds seq1 . n = seq . 0 ) implies Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 )
assume A1: for n being Element of NAT holds seq1 . n = seq . 0 ; :: thesis: Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1
A2: (((Partial_Sums seq) ^\ 1) - seq1) . 0 = (((Partial_Sums seq) ^\ 1) . 0 ) - (seq1 . 0 ) by NORMSP_1:def 6
.= (((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 BHSP_4:def 1
.= ((seq . (0 + 1)) + (seq . 0 )) - (seq . 0 ) by BHSP_4:def 1
.= (seq . (0 + 1)) + ((seq . 0 ) - (seq . 0 )) by RLVECT_1:def 6
.= (seq . (0 + 1)) + H₁(X) by RLVECT_1:28
.= seq . (0 + 1) by RLVECT_1:10
.= (seq ^\ 1) . 0 by NAT_1:def 3 ;

now

let n be Element of 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 6
.= (((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 BHSP_4:def 1
.= ((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 6
.= (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 6
.= ((((Partial_Sums seq) ^\ 1) - seq1) . n) + ((seq ^\ 1) . (n + 1)) by NAT_1:def 3 ; :: thesis: verum

end;

hence Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 by A2, BHSP_4:def 1; :: thesis: verum