let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for Cseq being Complex_Sequence
for n being Element of NAT holds (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Cseq * seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))
let seq be sequence of X; :: thesis: for Cseq being Complex_Sequence
for n being Element of NAT holds (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Cseq * seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))
let Cseq be Complex_Sequence; :: thesis: for n being Element of NAT holds (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n = ((Partial_Sums (Cseq * seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))
defpred S₁[ Element of NAT ] means (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . $1 = ((Partial_Sums (Cseq * seq)) . ($1 + 1)) - ((Cseq * (Partial_Sums seq)) . ($1 + 1));
A1: (Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . 0 = ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq)) . 0 by BHSP_4:def 1
.= ((Cseq - (Cseq ^\ 1)) . 0 ) * ((Partial_Sums seq) . 0 ) by Def9
.= ((Cseq + (- (Cseq ^\ 1))) . 0 ) * (seq . 0 ) by BHSP_4:def 1
.= ((Cseq . 0 ) + ((- (Cseq ^\ 1)) . 0 )) * (seq . 0 ) by VALUED_1:1
.= ((Cseq . 0 ) + (- ((Cseq ^\ 1) . 0 ))) * (seq . 0 ) by VALUED_1:8
.= ((Cseq . 0 ) - ((Cseq ^\ 1) . 0 )) * (seq . 0 )
.= ((Cseq . 0 ) - (Cseq . (0 + 1))) * (seq . 0 ) by NAT_1:def 3
.= ((Cseq . 0 ) * (seq . 0 )) - ((Cseq . 1) * (seq . 0 )) by CLVECT_1:11 ;
A2: (Cseq * (Partial_Sums seq)) . (0 + 1) = (Cseq . (0 + 1)) * ((Partial_Sums seq) . (0 + 1)) by Def9
.= (Cseq . (0 + 1)) * (((Partial_Sums seq) . 0 ) + (seq . (0 + 1))) by BHSP_4:def 1
.= (Cseq . 1) * ((seq . 0 ) + (seq . 1)) by BHSP_4:def 1
.= ((Cseq . 1) * (seq . 0 )) + ((Cseq . 1) * (seq . 1)) by CLVECT_1:def 2 ;

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 ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Cseq * seq)) . (n + 1)) - (((Cseq * (Partial_Sums seq)) . (n + 1)) - ((Cseq * (Partial_Sums seq)) . (n + 1))) by RLVECT_1:43;
then A4: ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1)) = ((Partial_Sums (Cseq * seq)) . (n + 1)) - H₁(X) by RLVECT_1:28;
(Partial_Sums (Cseq * seq)) . ((n + 1) + 1) = ((Partial_Sums (Cseq * seq)) . (n + 1)) + ((Cseq * seq) . ((n + 1) + 1)) by BHSP_4:def 1
.= (((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((Cseq * (Partial_Sums seq)) . (n + 1))) + ((Cseq * seq) . ((n + 1) + 1)) by A4, RLVECT_1:26
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Cseq * seq) . ((n + 1) + 1))) by RLVECT_1:def 6
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Cseq . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq * seq) . ((n + 1) + 1))) by Def9
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) - (Cseq . ((n + 1) + 1))) + (Cseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by Def9
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) - (Cseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by CLVECT_1:def 3
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) - ((Cseq ^\ 1) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by NAT_1:def 3
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) + (- ((Cseq ^\ 1) . (n + 1)))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq . (n + 1)) + ((- (Cseq ^\ 1)) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by VALUED_1:8
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by VALUED_1:1
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + ((((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) by RLVECT_1:def 6
.= (((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1)))) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by RLVECT_1:def 6
.= (((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq)) . (n + 1))) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by Def9
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) by BHSP_4:def 1
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + ((Cseq . ((n + 1) + 1)) * (((Partial_Sums seq) . (n + 1)) + (seq . ((n + 1) + 1)))) by CLVECT_1:def 2
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . ((n + 1) + 1))) by BHSP_4:def 1
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + ((Cseq * (Partial_Sums seq)) . ((n + 1) + 1)) by Def9 ;
then ((Partial_Sums (Cseq * seq)) . ((n + 1) + 1)) - ((Cseq * (Partial_Sums seq)) . ((n + 1) + 1)) = ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . (n + 1)) + (((Cseq * (Partial_Sums seq)) . ((n + 1) + 1)) - ((Cseq * (Partial_Sums seq)) . ((n + 1) + 1))) by RLVECT_1:def 6;
then ((Partial_Sums (Cseq * seq)) . ((n + 1) + 1)) - ((Cseq * (Partial_Sums seq)) . ((n + 1) + 1)) = ((Partial_Sums ((Cseq - (Cseq ^\ 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 (Cseq * seq)) . (0 + 1) = ((Partial_Sums (Cseq * seq)) . 0 ) + ((Cseq * seq) . (0 + 1)) by BHSP_4:def 1
.= ((Cseq * seq) . 0 ) + ((Cseq * seq) . 1) by BHSP_4:def 1
.= ((Cseq . 0 ) * (seq . 0 )) + ((Cseq * seq) . 1) by Def9
.= ((Cseq . 0 ) * (seq . 0 )) + ((Cseq . 1) * (seq . 1)) by Def9 ;
then (Partial_Sums (Cseq * seq)) . (0 + 1) = (((Cseq . 0 ) * (seq . 0 )) + H₁(X)) + ((Cseq . 1) * (seq . 1)) by RLVECT_1:10
.= (((Cseq . 0 ) * (seq . 0 )) + (((Cseq . 1) * (seq . 0 )) - ((Cseq . 1) * (seq . 0 )))) + ((Cseq . 1) * (seq . 1)) by RLVECT_1:28
.= ((((Cseq . 0 ) * (seq . 0 )) + (- ((Cseq . 1) * (seq . 0 )))) + ((Cseq . 1) * (seq . 0 ))) + ((Cseq . 1) * (seq . 1)) by RLVECT_1:def 6
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . 0 ) + ((Cseq * (Partial_Sums seq)) . (0 + 1)) by A1, A2, RLVECT_1:def 6 ;
then ((Partial_Sums (Cseq * seq)) . (0 + 1)) - ((Cseq * (Partial_Sums seq)) . (0 + 1)) = ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . 0 ) + (((Cseq * (Partial_Sums seq)) . (0 + 1)) - ((Cseq * (Partial_Sums seq)) . (0 + 1))) by RLVECT_1:def 6;
then ((Partial_Sums (Cseq * seq)) . (0 + 1)) - ((Cseq * (Partial_Sums seq)) . (0 + 1)) = ((Partial_Sums ((Cseq - (Cseq ^\ 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