let f be Function; :: thesis: ( f is Real_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is real ) ) )
thus ( f is Real_Sequence implies ( dom f = NAT & ( for x being set st x in NAT holds
f . x is real ) ) ) by FUNCT_2:def 1; :: thesis: ( dom f = NAT & ( for x being set st x in NAT holds
f . x is real ) implies f is Real_Sequence )
assume that
A3: dom f = NAT and
A4: for x being set st x in NAT holds
f . x is real ; :: thesis: f is Real_Sequence

now

let y be set ; :: thesis: ( y in rng f implies y in REAL )
assume y in rng f ; :: thesis: y in REAL
then consider x being set such that
A5: x in dom f and
A6: y = f . x by FUNCT_1:def 5;
f . x is real by A3, A4, A5;
hence y in REAL by A6, XREAL_0:def 1; :: thesis: verum

end;

then rng f c= REAL by TARSKI:def 3;
hence f is Real_Sequence by A3, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum