set f = PrimeNumbersS s;
thus rng (PrimeNumbersS s) c= SetPrimes by RELAT_1:def 19; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: SetPrimes c= rng (PrimeNumbersS s)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in SetPrimes or y in rng (PrimeNumbersS s) )
assume y in SetPrimes ; :: thesis: y in rng (PrimeNumbersS s)
then reconsider y = y as Prime by NEWTON:def 6;
set x = primeindex y;
A1: dom (PrimeNumbersS s) = NAT by FUNCT_2:def 1;
(PrimeNumbersS s) . (primeindex y) = primenumber (primeindex y) by Def3
.= y by NUMBER10:def 4 ;
hence y in rng (PrimeNumbersS s) by A1, FUNCT_1:def 3; :: thesis: verum