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

now :: thesis: for y being object st y in rng f holds
y in REAL

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

end;

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