let N be Nat; :: thesis: for f being Function holds
( f is Real_Sequence of N iff ( dom f = NAT & ( for n being Nat holds f . n is Point of (TOP-REAL N) ) ) )
let f be Function; :: thesis: ( f is Real_Sequence of N iff ( dom f = NAT & ( for n being Nat holds f . n is Point of (TOP-REAL N) ) ) )
thus ( f is Real_Sequence of N implies ( dom f = NAT & ( for n being Nat holds f . n is Point of (TOP-REAL N) ) ) ) by NORMSP_1:12, ORDINAL1:def 12; :: thesis: ( dom f = NAT & ( for n being Nat holds f . n is Point of (TOP-REAL N) ) implies f is Real_Sequence of N )
assume that
A1: dom f = NAT and
A2: for n being Nat holds f . n is Point of (TOP-REAL N) ; :: thesis: f is Real_Sequence of N
for x being set st x in NAT holds
f . x is Point of (TOP-REAL N) by A2;
hence f is Real_Sequence of N by A1, NORMSP_1:12; :: thesis: verum