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

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