let f be Function; :: thesis:
let RNS be non empty 1-sorted ; :: thesis:
let x be Element of RNS; :: thesis:
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:

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:

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:

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

let s be object ; :: thesis:
assume s in rng f ; :: thesis:
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:

end;

end;