let rseq be Real_Sequence; :: thesis: for cseq being Complex_Sequence st cseq = rseq holds
Partial_Product rseq = Partial_Product cseq
let cseq be Complex_Sequence; :: thesis: ( cseq = rseq implies Partial_Product rseq = Partial_Product cseq )
assume A1: cseq = rseq ; :: thesis: Partial_Product rseq = Partial_Product cseq
A3: dom (Partial_Product cseq) = NAT by COMSEQ_1:1
.= dom (Partial_Product rseq) by SEQ_1:1 ;
for k being Nat holds (Partial_Product cseq) . k = (Partial_Product rseq) . k

proof

let k be Nat; :: thesis: (Partial_Product cseq) . k = (Partial_Product rseq) . k
defpred S₁[ Nat] means (Partial_Product cseq) . $1 = (Partial_Product rseq) . $1;
B1: S₁[ 0 ]

proof

(Partial_Product cseq) . 0 = cseq . 0 by PP
.= (Partial_Product rseq) . 0 by A1, SERIES_3:def 1 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

B2: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume C1: S₁[j] ; :: thesis: S₁[j + 1]
(Partial_Product cseq) . (j + 1) = ((Partial_Product cseq) . j) * (cseq . (j + 1)) by PP
.= (Partial_Product rseq) . (j + 1) by A1, C1, SERIES_3:def 1 ;
hence S₁[j + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(B1, B2);
hence (Partial_Product cseq) . k = (Partial_Product rseq) . k ; :: thesis: verum

end;

hence Partial_Product rseq = Partial_Product cseq by A3; :: thesis: verum