let s be positive Nat; :: thesis: ( s >= 3 implies for f being Solution_of_Sierp169 of s holds rng (Solutions_of_Sierp168 f) c= { g where g is Solution_of_Sierp169 of s : verum } )
assume A1: s >= 3 ; :: thesis: for f being Solution_of_Sierp169 of s holds rng (Solutions_of_Sierp168 f) c= { g where g is Solution_of_Sierp169 of s : verum }
let f be Solution_of_Sierp169 of s; :: thesis: rng (Solutions_of_Sierp168 f) c= { g where g is Solution_of_Sierp169 of s : verum }
set F = Solutions_of_Sierp168 f;
set A = { g where g is Solution_of_Sierp169 of s : verum } ;
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_Sierp169 of s : verum } )
assume y in rng (Solutions_of_Sierp168 f) ; :: thesis: y in { g where g is Solution_of_Sierp169 of s : verum }
then consider x being object such that
A2: x in dom (Solutions_of_Sierp168 f) and
A3: (Solutions_of_Sierp168 f) . x = y by FUNCT_1:def 3;
reconsider x = x as Element of NATPLUS by A2;
f is a_solution_of_Sierp169 by A1, Def18;
then A4: x (#) f is a_solution_of_Sierp169 by Th146;
(Solutions_of_Sierp168 f) . x = x (#) f by NUMBER15:def 15;
then y is Solution_of_Sierp169 of s by A1, A3, A4, Def18;
hence y in { g where g is Solution_of_Sierp169 of s : verum } ; :: thesis: verum