let f be Function; :: thesis: ( f is Complex_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of COMPLEX ) ) )
thus ( f is Complex_Sequence implies ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of COMPLEX ) ) ) :: thesis: ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of COMPLEX ) implies f is Complex_Sequence )

proof

assume A1: f is Complex_Sequence ; :: thesis: ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of COMPLEX ) )
hence A2: dom f = NAT by FUNCT_2:def 1; :: thesis: for x being set st x in NAT holds
f . x is Element of COMPLEX
let x be set ; :: thesis: ( x in NAT implies f . x is Element of COMPLEX )
assume x in NAT ; :: thesis: f . x is Element of COMPLEX
then A3: f . x in rng f by A2, FUNCT_1:def 3;
rng f c= COMPLEX by A1, RELAT_1:def 19;
hence f . x is Element of COMPLEX by A3; :: thesis: verum

end;

assume that
A4: dom f = NAT and
A5: for x being set st x in NAT holds
f . x is Element of COMPLEX ; :: thesis: f is Complex_Sequence

now :: thesis: for y being object st y in rng f holds
y in COMPLEX

let y be object ; :: thesis: ( y in rng f implies y in COMPLEX )
assume y in rng f ; :: thesis: y in COMPLEX
then consider x being object such that
A6: x in dom f and
A7: y = f . x by FUNCT_1:def 3;
f . x is Element of COMPLEX by A4, A5, A6;
hence y in COMPLEX by A7; :: thesis: verum

end;

then rng f c= COMPLEX by TARSKI:def 3;
hence f is Complex_Sequence by A4, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum