let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 exampleSierpinski196 or not x2 in proj1 exampleSierpinski196 or not exampleSierpinski196 . x1 = exampleSierpinski196 . x2 or x1 = x2 )
assume ( x1 in dom exampleSierpinski196 & x2 in dom exampleSierpinski196 ) ; :: thesis: ( not exampleSierpinski196 . x1 = exampleSierpinski196 . x2 or x1 = x2 )
then reconsider x1 = x1, x2 = x2 as Element of NAT ;
( exampleSierpinski196 . x1 = H₅(x1) & exampleSierpinski196 . x2 = H₅(x2) ) by Def16;
hence ( not exampleSierpinski196 . x1 = exampleSierpinski196 . x2 or x1 = x2 ) by XTUPLE_0:5; :: thesis: verum