deffunc H₁( Element of NAT ) -> Element of NAT = 0 ;
consider bseq being Real_Sequence such that
A1: for n being Element of NAT holds bseq . n = H₁(n) from SEQ_1:sch 1();
let seq be Real_Sequence; :: thesis: for cseq being Complex_Sequence st seq = cseq holds
( seq is convergent iff cseq is convergent )
let cseq be Complex_Sequence; :: thesis: ( seq = cseq implies ( seq is convergent iff cseq is convergent ) )
assume A2: seq = cseq ; :: thesis: ( seq is convergent iff cseq is convergent )
A3: for n being Element of NAT holds
( Re (cseq . n) = seq . n & Im (cseq . n) = bseq . n )

proof

let n be Element of NAT ; :: thesis: ( Re (cseq . n) = seq . n & Im (cseq . n) = bseq . n )
thus Re (cseq . n) = seq . n by A2, COMPLEX1:def 1; :: thesis: Im (cseq . n) = bseq . n
Im (cseq . n) = Im (seq . n) by A2;
then Im (cseq . n) = 0 by COMPLEX1:def 2;
hence Im (cseq . n) = bseq . n by A1; :: thesis: verum

end;

now

let n be Nat; :: thesis: bseq . n = 0
n in NAT by ORDINAL1:def 12;
hence bseq . n = 0 by A1; :: thesis: verum

end;

then bseq is constant by VALUED_0:def 18;
hence ( seq is convergent iff cseq is convergent ) by A3, COMSEQ_3:38; :: thesis: verum