let x, y, z be object ; :: thesis: ( x <> y & x <> z & y <> z implies <%x,y,z%> is one-to-one )
assume A1: ( x <> y & x <> z & y <> z ) ; :: thesis: <%x,y,z%> is one-to-one

now :: thesis: for x1, x2 being object st x1 in dom <%x,y,z%> & x2 in dom <%x,y,z%> & <%x,y,z%> . x1 = <%x,y,z%> . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom <%x,y,z%> & x2 in dom <%x,y,z%> & <%x,y,z%> . x1 = <%x,y,z%> . x2 implies b₁ = b₂ )
assume A2: ( x1 in dom <%x,y,z%> & x2 in dom <%x,y,z%> & <%x,y,z%> . x1 = <%x,y,z%> . x2 ) ; :: thesis: b₁ = b₂
then ( x1 in {0,1,2} & x2 in {0,1,2} ) by Th8;

per cases then ( ( x1 = 0 & ( x2 = 0 or x2 = 1 or x2 = 2 ) ) or ( x1 = 1 & ( x2 = 0 or x2 = 1 or x2 = 2 ) ) or ( x1 = 2 & ( x2 = 0 or x2 = 1 or x2 = 2 ) ) ) by ENUMSET1:def 1;

suppose ( x1 = 0 & ( x2 = 0 or x2 = 1 or x2 = 2 ) ) ; :: thesis: b₁ = b₂

hence x1 = x2 by A1, A2; :: thesis: verum

end;

suppose ( x1 = 1 & ( x2 = 0 or x2 = 1 or x2 = 2 ) ) ; :: thesis: b₁ = b₂

hence x1 = x2 by A1, A2; :: thesis: verum

end;

suppose ( x1 = 2 & ( x2 = 0 or x2 = 1 or x2 = 2 ) ) ; :: thesis: b₁ = b₂

hence x1 = x2 by A1, A2; :: thesis: verum

end;

end;

end;

hence <%x,y,z%> is one-to-one by FUNCT_1:def 4; :: thesis: verum