let f be Function; :: thesis: ( f is Complex_Sequence iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) ) )

thus ( f is Complex_Sequence implies ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) ) ) by Th1; :: thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) implies f is Complex_Sequence )

assume that

A1: dom f = NAT and

A2: for n being Element of NAT holds f . n is Element of COMPLEX ; :: thesis: f is Complex_Sequence

for x being set st x in NAT holds

f . x is Element of COMPLEX by A2;

hence f is Complex_Sequence by A1, Th1; :: thesis: verum

thus ( f is Complex_Sequence implies ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) ) ) by Th1; :: thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) implies f is Complex_Sequence )

assume that

A1: dom f = NAT and

A2: for n being Element of NAT holds f . n is Element of COMPLEX ; :: thesis: f is Complex_Sequence

for x being set st x in NAT holds

f . x is Element of COMPLEX by A2;

hence f is Complex_Sequence by A1, Th1; :: thesis: verum