let N be non empty MetrStruct ; :: thesis: for f being Function holds
( f is sequence of N iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of N ) ) )
let f be Function; :: thesis: ( f is sequence of N iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of N ) ) )
thus ( f is sequence of N implies ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of N ) ) ) :: thesis: ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of N ) implies f is sequence of N )

proof

assume A1: f is sequence of N ; :: thesis: ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of N ) )
hence dom f = NAT by FUNCT_2:def 1; :: thesis: for x being set st x in NAT holds
f . x is Element of N
let x be set ; :: thesis: ( x in NAT implies f . x is Element of N )
assume x in NAT ; :: thesis: f . x is Element of N
then x in dom f by A1, FUNCT_2:def 1;
then A2: f . x in rng f by FUNCT_1:def 3;
rng f c= the carrier of N by A1, RELAT_1:def 19;
hence f . x is Element of N by A2; :: thesis: verum

end;

assume that
A3: dom f = NAT and
A4: for x being set st x in NAT holds
f . x is Element of N ; :: thesis: f is sequence of N

now :: thesis: for y being object st y in rng f holds
y in the carrier of N

let y be object ; :: thesis: ( y in rng f implies y in the carrier of N )
assume y in rng f ; :: thesis: y in the carrier of N
then consider x being object such that
A5: x in dom f and
A6: y = f . x by FUNCT_1:def 3;
f . x is Element of N by A3, A4, A5;
hence y in the carrier of N by A6; :: thesis: verum

end;

then rng f c= the carrier of N ;
hence f is sequence of N by A3, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum