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