let f be Function; :: thesis: ( f is Real_Sequence iff ( dom f = NAT & ( for n being Element of NAT holds f . n is real ) ) )
thus ( f is Real_Sequence implies ( dom f = NAT & ( for n being Element of NAT holds f . n is real ) ) ) by Th3; :: thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n is real ) implies f is Real_Sequence )
assume that
A1: dom f = NAT and
A2: for n being Element of NAT holds f . n is real ; :: thesis: f is Real_Sequence
for x being set st x in NAT holds
f . x is real by A2;
hence f is Real_Sequence by A1, Th3; :: thesis: verum