let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for Cseq being Complex_Sequence
for n being 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 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 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₁[ 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 Def8
.= ((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:10 ;
A2: (Cseq * (Partial_Sums seq)) . (0 + 1) = (Cseq . (0 + 1)) * ((Partial_Sums seq) . (0 + 1)) by Def8
.= (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 :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be 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:29;
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:15;
(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:13
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Cseq * (Partial_Sums seq)) . (n + 1)) + ((Cseq * seq) . ((n + 1) + 1))) by RLVECT_1:def 3
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . n) + (((Cseq . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq * seq) . ((n + 1) + 1))) by Def8
.= ((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 Def8
.= ((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 3
.= (((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 3
.= (((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 Def8
.= ((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 Def8 ;
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 3;
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:15;
hence S₁[n + 1] by RLVECT_1:4; :: 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 Def8
.= ((Cseq . 0) * (seq . 0)) + ((Cseq . 1) * (seq . 1)) by Def8 ;
then (Partial_Sums (Cseq * seq)) . (0 + 1) = (((Cseq . 0) * (seq . 0)) + H₁(X)) + ((Cseq . 1) * (seq . 1)) by RLVECT_1:4
.= (((Cseq . 0) * (seq . 0)) + (((Cseq . 1) * (seq . 0)) - ((Cseq . 1) * (seq . 0)))) + ((Cseq . 1) * (seq . 1)) by RLVECT_1:15
.= ((((Cseq . 0) * (seq . 0)) + (- ((Cseq . 1) * (seq . 0)))) + ((Cseq . 1) * (seq . 0))) + ((Cseq . 1) * (seq . 1)) by RLVECT_1:def 3
.= ((Partial_Sums ((Cseq - (Cseq ^\ 1)) * (Partial_Sums seq))) . 0) + ((Cseq * (Partial_Sums seq)) . (0 + 1)) by A1, A2, RLVECT_1:def 3 ;
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 3;
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:15;
then A5: S₁[ 0 ] by RLVECT_1:4;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A3); :: thesis: verum