let Rseq be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X
for n being Element of NAT holds (Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Rseq * seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))
let X be RealUnitarySpace; :: thesis: for seq being sequence of X
for n being Element of NAT holds (Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Rseq * seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))
let seq be sequence of X; :: thesis: for n being Element of NAT holds (Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Rseq * seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))
defpred S₁[ Element of NAT ] means (Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . $1 = ((Partial_Sums (Rseq * seq)) . ($1 + 1)) - ((Rseq * (Partial_Sums seq)) . ($1 + 1));
A1: (Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . 0 = ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq)) . 0 by Def1
.= ((Rseq - (Rseq ^\ 1)) . 0 ) * ((Partial_Sums seq) . 0 ) by Def9
.= ((Rseq + (- (Rseq ^\ 1))) . 0 ) * (seq . 0 ) by Def1
.= ((Rseq . 0 ) + ((- (Rseq ^\ 1)) . 0 )) * (seq . 0 ) by SEQ_1:11
.= ((Rseq . 0 ) + (- ((Rseq ^\ 1) . 0 ))) * (seq . 0 ) by SEQ_1:14
.= ((Rseq . 0 ) - ((Rseq ^\ 1) . 0 )) * (seq . 0 )
.= ((Rseq . 0 ) - (Rseq . (0 + 1))) * (seq . 0 ) by NAT_1:def 3
.= ((Rseq . 0 ) * (seq . 0 )) - ((Rseq . 1) * (seq . 0 )) by RLVECT_1:49 ;
A2: (Rseq * (Partial_Sums seq)) . (0 + 1) = (Rseq . (0 + 1)) * ((Partial_Sums seq) . (0 + 1)) by Def9
.= (Rseq . (0 + 1)) * (((Partial_Sums seq) . 0 ) + (seq . (0 + 1))) by Def1
.= (Rseq . 1) * ((seq . 0 ) + (seq . 1)) by Def1
.= ((Rseq . 1) * (seq . 0 )) + ((Rseq . 1) * (seq . 1)) by RLVECT_1:def 8 ;

A3: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Rseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Rseq * seq)) . (n + 1)) - (((Rseq * (Partial_Sums seq)) . (n + 1)) - ((Rseq * (Partial_Sums seq)) . (n + 1))) by RLVECT_1:43;
then A4: ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Rseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Rseq * seq)) . (n + 1)) - H₁(X) by RLVECT_1:28;
(Partial_Sums (Rseq * seq)) . ((n + 1) + 1) = ((Partial_Sums (Rseq * seq)) . (n + 1)) + ((Rseq * seq) . ((n + 1) + 1)) by Def1
.= (((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Rseq * (Partial_Sums seq)) . (n + 1))) + ((Rseq * seq) . ((n + 1) + 1)) by A4, RLVECT_1:26
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Rseq * (Partial_Sums seq)) . (n + 1)) + ((Rseq * seq) . ((n + 1) + 1))) by RLVECT_1:def 6
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Rseq . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Rseq * seq) . ((n + 1) + 1))) by Def9
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Rseq . (n + 1)) - (Rseq . ((n + 1) + 1))) + (Rseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by Def9
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Rseq . (n + 1)) - (Rseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by RLVECT_1:def 9
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Rseq . (n + 1)) - ((Rseq ^\ 1) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by NAT_1:def 3
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Rseq . (n + 1)) + (- ((Rseq ^\ 1) . (n + 1)))) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Rseq . (n + 1)) + ((- (Rseq ^\ 1)) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by SEQ_1:14
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Rseq - (Rseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by SEQ_1:11
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + ((((Rseq - (Rseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + (((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by RLVECT_1:def 6
.= (((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Rseq - (Rseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1)))) + (((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by RLVECT_1:def 6
.= (((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq)) . (n + 1))) + (((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by Def9
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + (((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Rseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by Def1
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + ((Rseq . ((n + 1) + 1)) * (((Partial_Sums seq) . (n + 1)) + (seq . ((n + 1) + 1)))) by RLVECT_1:def 8
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + ((Rseq . ((n + 1) + 1)) * ((Partial_Sums seq) . ((n + 1) + 1))) by Def1
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + ((Rseq * (Partial_Sums seq)) . ((n + 1) + 1)) by Def9 ;
then ((Partial_Sums (Rseq * seq)) . ((n + 1) + 1)) - ((Rseq * (Partial_Sums seq)) . ((n + 1) + 1)) = ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + (((Rseq * (Partial_Sums seq)) . ((n + 1) + 1)) - ((Rseq * (Partial_Sums seq)) . ((n + 1) + 1))) by RLVECT_1:def 6;
then ((Partial_Sums (Rseq * seq)) . ((n + 1) + 1)) - ((Rseq * (Partial_Sums seq)) . ((n + 1) + 1)) = ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + H₁(X) by RLVECT_1:28;
hence S₁[n + 1] by RLVECT_1:10; :: thesis: verum

end;

(Partial_Sums (Rseq * seq)) . (0 + 1) = ((Partial_Sums (Rseq * seq)) . 0 ) + ((Rseq * seq) . (0 + 1)) by Def1
.= ((Rseq * seq) . 0 ) + ((Rseq * seq) . 1) by Def1
.= ((Rseq . 0 ) * (seq . 0 )) + ((Rseq * seq) . 1) by Def9
.= ((Rseq . 0 ) * (seq . 0 )) + ((Rseq . 1) * (seq . 1)) by Def9 ;
then (Partial_Sums (Rseq * seq)) . (0 + 1) = (((Rseq . 0 ) * (seq . 0 )) + H₁(X)) + ((Rseq . 1) * (seq . 1)) by RLVECT_1:10
.= (((Rseq . 0 ) * (seq . 0 )) + (((Rseq . 1) * (seq . 0 )) - ((Rseq . 1) * (seq . 0 )))) + ((Rseq . 1) * (seq . 1)) by RLVECT_1:28
.= ((((Rseq . 0 ) * (seq . 0 )) + (- ((Rseq . 1) * (seq . 0 )))) + ((Rseq . 1) * (seq . 0 ))) + ((Rseq . 1) * (seq . 1)) by RLVECT_1:def 6
.= ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . 0 ) + ((Rseq * (Partial_Sums seq)) . (0 + 1)) by A1, A2, RLVECT_1:def 6 ;
then ((Partial_Sums (Rseq * seq)) . (0 + 1)) - ((Rseq * (Partial_Sums seq)) . (0 + 1)) = ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . 0 ) + (((Rseq * (Partial_Sums seq)) . (0 + 1)) - ((Rseq * (Partial_Sums seq)) . (0 + 1))) by RLVECT_1:def 6;
then ((Partial_Sums (Rseq * seq)) . (0 + 1)) - ((Rseq * (Partial_Sums seq)) . (0 + 1)) = ((Partial_Sums ((Rseq - (Rseq ^\ 1)) * (Partial_Sums seq))) . 0 ) + H₁(X) by RLVECT_1:28;
then A5: S₁[ 0 ] by RLVECT_1:10;
thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A5, A3); :: thesis: verum