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