let s be positive Nat; :: thesis: for f being Solution_of_Sierp168 of s holds rng (Solutions_of_Sierp168 f) c= { g where g is Solution_of_Sierp168 of s : verum }
let f be Solution_of_Sierp168 of s; :: thesis: rng (Solutions_of_Sierp168 f) c= { g where g is Solution_of_Sierp168 of s : verum }
set F = Solutions_of_Sierp168 f;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Solutions_of_Sierp168 f) or y in { g where g is Solution_of_Sierp168 of s : verum } )
assume y in rng (Solutions_of_Sierp168 f) ; :: thesis: y in { g where g is Solution_of_Sierp168 of s : verum }
then consider x being object such that
A1: x in dom (Solutions_of_Sierp168 f) and
A2: (Solutions_of_Sierp168 f) . x = y by FUNCT_1:def 3;
reconsider x = x as Element of NATPLUS by A1;
(Solutions_of_Sierp168 f) . x = x (#) f by Def15;
then y is Solution_of_Sierp168 of s by A2, Def14;
hence y in { g where g is Solution_of_Sierp168 of s : verum } ; :: thesis: verum