let Rseq be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X
for n being 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 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 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₁[ 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 Def7
.= ((Rseq + (- (Rseq ^\ 1))) . 0) * (seq . 0) by Def1
.= ((Rseq . 0) + ((- (Rseq ^\ 1)) . 0)) * (seq . 0) by SEQ_1:7
.= ((Rseq . 0) + (- ((Rseq ^\ 1) . 0))) * (seq . 0) by SEQ_1:10
.= ((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:35 ;
A2: (Rseq * (Partial_Sums seq)) . (0 + 1) = (Rseq . (0 + 1)) * ((Partial_Sums seq) . (0 + 1)) by Def7
.= (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 5 ;

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