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 ;
then A2: f . x in rng f by FUNCT_1:def 3;
rng f c= the carrier of N by ;
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 ; :: thesis: verum