let w, z be Complex; :: thesis: for k being Nat holds (((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums ((z + w) ExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k
let k be Nat; :: thesis: (((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums ((z + w) ExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k
A1: k in NAT by ORDINAL1:def 12;
A2: (((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums ((z + w) ExpSeq)) . k) = (((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums (Alfa (k,z,w))) . k) by Th14
.= ((((Partial_Sums (w ExpSeq)) . k) (#) (Partial_Sums (z ExpSeq))) . k) - ((Partial_Sums (Alfa (k,z,w))) . k) by VALUED_1:6
.= ((Partial_Sums (((Partial_Sums (w ExpSeq)) . k) (#) (z ExpSeq))) . k) - ((Partial_Sums (Alfa (k,z,w))) . k) by COMSEQ_3:29
.= ((Partial_Sums (((Partial_Sums (w ExpSeq)) . k) (#) (z ExpSeq))) . k) + ((- (Partial_Sums (Alfa (k,z,w)))) . k) by VALUED_1:8
.= ((Partial_Sums (((Partial_Sums (w ExpSeq)) . k) (#) (z ExpSeq))) - (Partial_Sums (Alfa (k,z,w)))) . k by VALUED_1:1, A1
.= (Partial_Sums ((((Partial_Sums (w ExpSeq)) . k) (#) (z ExpSeq)) - (Alfa (k,z,w)))) . k by COMSEQ_3:28 ;
for l being Nat st l <= k holds
((((Partial_Sums (w ExpSeq)) . k) (#) (z ExpSeq)) - (Alfa (k,z,w))) . l = (Conj (k,z,w)) . l
proof
let l be Nat; :: thesis: ( l <= k implies ((((Partial_Sums (w ExpSeq)) . k) (#) (z ExpSeq)) - (Alfa (k,z,w))) . l = (Conj (k,z,w)) . l )
assume A3: l <= k ; :: thesis: ((((Partial_Sums (w ExpSeq)) . k) (#) (z ExpSeq)) - (Alfa (k,z,w))) . l = (Conj (k,z,w)) . l
A4: l in NAT by ORDINAL1:def 12;
thus ((((Partial_Sums (w ExpSeq)) . k) (#) (z ExpSeq)) - (Alfa (k,z,w))) . l = ((((Partial_Sums (w ExpSeq)) . k) (#) (z ExpSeq)) . l) + ((- (Alfa (k,z,w))) . l) by VALUED_1:1, A4
.= ((((Partial_Sums (w ExpSeq)) . k) (#) (z ExpSeq)) . l) - ((Alfa (k,z,w)) . l) by VALUED_1:8
.= (((Partial_Sums (w ExpSeq)) . k) * ((z ExpSeq) . l)) - ((Alfa (k,z,w)) . l) by VALUED_1:6
.= (((z ExpSeq) . l) * ((Partial_Sums (w ExpSeq)) . k)) - (((z ExpSeq) . l) * ((Partial_Sums (w ExpSeq)) . (k -' l))) by A3, Def11
.= ((z ExpSeq) . l) * (((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l)))
.= (Conj (k,z,w)) . l by A3, Def13 ; :: thesis: verum
end;
hence (((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums ((z + w) ExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k by A2, COMSEQ_3:35; :: thesis: verum