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

hence f is Real_Sequence by A1, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

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

then
rng f c= REAL
by TARSKI:def 3;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;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

hence f is Real_Sequence by A1, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum