let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng exampleSierpinski149 or y in { [x,y,z] where x, y, z is negative Integer : (((4 * x) * y) - x) - y = z ^2 } )
assume y in rng exampleSierpinski149 ; :: thesis: y in { [x,y,z] where x, y, z is negative Integer : (((4 * x) * y) - x) - y = z ^2 }
then consider k being object such that
A1: k in dom exampleSierpinski149 and
A2: exampleSierpinski149 . k = y by FUNCT_1:def 3;
reconsider k = k as Element of NATPLUS by A1;
(((4 * H₁(k)) * H₂(k)) - H₁(k)) - H₂(k) = H₃(k) ^2 ;
then H₄(k) in { [x,y,z] where x, y, z is negative Integer : (((4 * x) * y) - x) - y = z ^2 } ;
hence y in { [x,y,z] where x, y, z is negative Integer : (((4 * x) * y) - x) - y = z ^2 } by A2, Def18; :: thesis: verum