let N be non empty MetrStruct ; :: thesis: for f being Function holds

( f is sequence of N iff ( dom f = NAT & ( for n being Nat holds f . n is Element of N ) ) )

let f be Function; :: thesis: ( f is sequence of N iff ( dom f = NAT & ( for n being Nat holds f . n is Element of N ) ) )

thus ( f is sequence of N implies ( dom f = NAT & ( for n being Nat holds f . n is Element of N ) ) ) by Lm1, ORDINAL1:def 12; :: thesis: ( dom f = NAT & ( for n being Nat holds f . n is Element of N ) implies f is sequence of N )

assume that

A1: dom f = NAT and

A2: for n being Nat holds f . n is Element of N ; :: thesis: f is sequence of N

for x being set st x in NAT holds

f . x is Element of N by A2;

hence f is sequence of N by A1, Lm1; :: thesis: verum

( f is sequence of N iff ( dom f = NAT & ( for n being Nat holds f . n is Element of N ) ) )

let f be Function; :: thesis: ( f is sequence of N iff ( dom f = NAT & ( for n being Nat holds f . n is Element of N ) ) )

thus ( f is sequence of N implies ( dom f = NAT & ( for n being Nat holds f . n is Element of N ) ) ) by Lm1, ORDINAL1:def 12; :: thesis: ( dom f = NAT & ( for n being Nat holds f . n is Element of N ) implies f is sequence of N )

assume that

A1: dom f = NAT and

A2: for n being Nat holds f . n is Element of N ; :: thesis: f is sequence of N

for x being set st x in NAT holds

f . x is Element of N by A2;

hence f is sequence of N by A1, Lm1; :: thesis: verum