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 )

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

hence f is Complex_Sequence by A4, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

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 that
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;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

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

then
rng f c= COMPLEX
by TARSKI:def 3;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;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

hence f is Complex_Sequence by A4, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum