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 )

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

hence f is sequence of N by A3, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

( 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 that
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;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

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

then
rng f c= the carrier of N
;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;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

hence f is sequence of N by A3, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum