set f = exampleSierpinski150 (m,D);
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 (exampleSierpinski150 (m,D)) or not x2 in proj1 (exampleSierpinski150 (m,D)) or not (exampleSierpinski150 (m,D)) . x1 = (exampleSierpinski150 (m,D)) . x2 or x1 = x2 )
assume that
A1: ( x1 in dom (exampleSierpinski150 (m,D)) & x2 in dom (exampleSierpinski150 (m,D)) ) and
A2: (exampleSierpinski150 (m,D)) . x1 = (exampleSierpinski150 (m,D)) . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of NAT by A1;

now :: thesis: not x1 <> x2

assume x1 <> x2 ; :: thesis: contradiction
then ( x1 < x2 or x2 < x1 ) by XXREAL_0:1;
then ( ((exampleSierpinski150 (m,D)) . x1) `1 < ((exampleSierpinski150 (m,D)) . x2) `1 or ((exampleSierpinski150 (m,D)) . x2) `1 < ((exampleSierpinski150 (m,D)) . x1) `1 ) by Th98;
hence contradiction by A2; :: thesis: verum

end;

hence x1 = x2 ; :: thesis: verum