let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 exampleSierpinski149 or not x2 in proj1 exampleSierpinski149 or not exampleSierpinski149 . x1 = exampleSierpinski149 . x2 or x1 = x2 )
assume that
A1: ( x1 in dom exampleSierpinski149 & x2 in dom exampleSierpinski149 ) and
A2: exampleSierpinski149 . x1 = exampleSierpinski149 . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of NATPLUS by A1;
( exampleSierpinski149 . x1 = H₄(x1) & exampleSierpinski149 . x2 = H₄(x2) ) by Def18;
then (- (5 * x1)) - 1 = (- (5 * x2)) - 1 by A2, XTUPLE_0:3;
hence x1 = x2 ; :: thesis: verum