let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng exampleSierpinski196 or y in { [x,y,z,t] where x, y, z, t is Integer : ( x + y = z * t & z + t = x * y ) } )
assume y in rng exampleSierpinski196 ; :: thesis: y in { [x,y,z,t] where x, y, z, t is Integer : ( x + y = z * t & z + t = x * y ) }
then consider k being object such that
A1: k in dom exampleSierpinski196 and
A2: exampleSierpinski196 . k = y by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A1;
( H₁(k) + H₂(k) = H₃(k) * H₄(k) & H₃(k) + H₄(k) = H₁(k) * H₂(k) ) ;
then H₅(k) in { [x,y,z,t] where x, y, z, t is Integer : ( x + y = z * t & z + t = x * y ) } ;
hence y in { [x,y,z,t] where x, y, z, t is Integer : ( x + y = z * t & z + t = x * y ) } by A2, Def16; :: thesis: verum