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

proof

assume A1: f is sequence of RNS ; :: thesis: ( dom f = NAT & ( for d being set st d in NAT holds
f . d is Element of RNS ) )
then A2: rng f c= the carrier of RNS by RELAT_1:def 19;
A3: dom f = NAT by A1, FUNCT_2:def 1;
for d being set st d in NAT holds
f . d is Element of RNS

proof

let d be set ; :: thesis: ( d in NAT implies f . d is Element of RNS )
assume d in NAT ; :: thesis: f . d is Element of RNS
then f . d in rng f by A3, FUNCT_1:def 3;
hence f . d is Element of RNS by A2; :: thesis: verum

end;

hence ( dom f = NAT & ( for d being set st d in NAT holds
f . d is Element of RNS ) ) by A1, FUNCT_2:def 1; :: thesis: verum

end;

thus ( dom f = NAT & ( for d being set st d in NAT holds
f . d is Element of RNS ) implies f is sequence of RNS ) :: thesis: verum

proof

assume that
A4: dom f = NAT and
A5: for d being set st d in NAT holds
f . d is Element of RNS ; :: thesis: f is sequence of RNS
for s being object st s in rng f holds
s in the carrier of RNS

proof

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

end;

then rng f c= the carrier of RNS by TARSKI:def 3;
hence f is sequence of RNS by A4, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

end;