deffunc H₁( Nat) -> Element of NAT = 0 ;
let rs be Real_Sequence; :: thesis: for cs being Complex_Sequence st rs = cs & rs is convergent holds
cs is convergent
let cs be Complex_Sequence; :: thesis: ( rs = cs & rs is convergent implies cs is convergent )
assume that
A1: rs = cs and
A2: rs is convergent ; :: thesis: cs is convergent
consider bs being Real_Sequence such that
A3: for n being Element of NAT holds bs . n = H₁(n) from SEQ_1:sch 1();
for n being Nat holds bs . n = H₁(n)

proof

let n be Nat; :: thesis: bs . n = H₁(n)
n in NAT by ORDINAL1:def 13;
hence bs . n = H₁(n) by A3; :: thesis: verum

end;

then A4: bs is constant by VALUED_0:def 18;
for n being Element of NAT holds
( Re (cs . n) = rs . n & Im (cs . n) = bs . n )

proof

let n be Element of NAT ; :: thesis: ( Re (cs . n) = rs . n & Im (cs . n) = bs . n )
thus Re (cs . n) = rs . n by A1, COMPLEX1:def 2; :: thesis: Im (cs . n) = bs . n
Im (cs . n) = Im (rs . n) by A1;
then Im (cs . n) = 0 by COMPLEX1:def 3;
hence Im (cs . n) = bs . n by A3; :: thesis: verum

end;

hence cs is convergent by A2, A4, COMSEQ_3:38; :: thesis: verum