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

A2: now :: thesis: for k being Nat holds (((Partial_Sums s) ^\ 1) - s1) . (k + 1) = ((((Partial_Sums s) ^\ 1) - s1) . k) + ((s ^\ 1) . (k + 1))

let k be Nat; :: thesis: (((Partial_Sums s) ^\ 1) - s1) . (k + 1) = ((((Partial_Sums s) ^\ 1) - s1) . k) + ((s ^\ 1) . (k + 1))
thus (((Partial_Sums s) ^\ 1) - s1) . (k + 1) = (((Partial_Sums s) ^\ 1) . (k + 1)) - (s1 . (k + 1)) by NORMSP_1:def 3
.= (((Partial_Sums s) ^\ 1) . (k + 1)) - (s . 0) by A1
.= ((Partial_Sums s) . ((k + 1) + 1)) - (s . 0) by NAT_1:def 3
.= ((s . ((k + 1) + 1)) + ((Partial_Sums s) . (k + 1))) - (s . 0) by BHSP_4:def 1
.= ((s . ((k + 1) + 1)) + ((Partial_Sums s) . (k + 1))) - (s1 . k) by A1
.= (s . ((k + 1) + 1)) + (((Partial_Sums s) . (k + 1)) - (s1 . k)) by RLVECT_1:def 3
.= (s . ((k + 1) + 1)) + ((((Partial_Sums s) ^\ 1) . k) - (s1 . k)) by NAT_1:def 3
.= (s . ((k + 1) + 1)) + ((((Partial_Sums s) ^\ 1) - s1) . k) by NORMSP_1:def 3
.= ((((Partial_Sums s) ^\ 1) - s1) . k) + ((s ^\ 1) . (k + 1)) by NAT_1:def 3 ; :: thesis: verum

end;

(((Partial_Sums s) ^\ 1) - s1) . 0 = (((Partial_Sums s) ^\ 1) . 0) - (s1 . 0) by NORMSP_1:def 3
.= (((Partial_Sums s) ^\ 1) . 0) - (s . 0) by A1
.= ((Partial_Sums s) . (0 + 1)) - (s . 0) by NAT_1:def 3
.= (((Partial_Sums s) . 0) + (s . (0 + 1))) - (s . 0) by BHSP_4:def 1
.= ((s . (0 + 1)) + (s . 0)) - (s . 0) by BHSP_4:def 1
.= (s . (0 + 1)) + ((s . 0) - (s . 0)) by RLVECT_1:def 3
.= (s . (0 + 1)) + (0. X) by RLVECT_1:15
.= s . (0 + 1) by RLVECT_1:4
.= (s ^\ 1) . 0 by NAT_1:def 3 ;
hence Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 by A2, BHSP_4:def 1; :: thesis: verum