let RNS be non empty 1-sorted ; :: thesis: for x being Element of RNS ex S being sequence of RNS st rng S = {x}
let x be Element of RNS; :: thesis: ex S being sequence of RNS st rng S = {x}
consider f being Function such that
A1: dom f = NAT and
A2: rng f = {x} by FUNCT_1:5;
reconsider f = f as sequence of RNS by A1, A2, FUNCT_2:def 1, RELSET_1:4;
take f ; :: thesis: rng f = {x}
thus rng f = {x} by A2; :: thesis: verum