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