let X be set ; :: thesis: for n being Nat holds canon_image (X,n) is one-to-one
let n be Nat; :: thesis: canon_image (X,n) is one-to-one
for x1, x2 being object st x1 in dom (canon_image (X,n)) & x2 in dom (canon_image (X,n)) & (canon_image (X,n)) . x1 = (canon_image (X,n)) . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom (canon_image (X,n)) & x2 in dom (canon_image (X,n)) & (canon_image (X,n)) . x1 = (canon_image (X,n)) . x2 implies x1 = x2 )
assume A1: ( x1 in dom (canon_image (X,n)) & x2 in dom (canon_image (X,n)) ) ; :: thesis: ( not (canon_image (X,n)) . x1 = (canon_image (X,n)) . x2 or x1 = x2 )
assume A2: (canon_image (X,n)) . x1 = (canon_image (X,n)) . x2 ; :: thesis: x1 = x2

per cases ( n > 0 or not n > 0 ) ;

suppose n > 0 ; :: thesis: x1 = x2

then ( (canon_image (X,n)) . x1 = [x1,n] & (canon_image (X,n)) . x2 = [x2,n] ) by A1, Def19;
hence x1 = x2 by A2, XTUPLE_0:1; :: thesis: verum

end;

suppose not n > 0 ; :: thesis: x1 = x2

then canon_image (X,n) = {} by Def19;
hence x1 = x2 by A1; :: thesis: verum

end;

end;

end;

hence canon_image (X,n) is one-to-one by FUNCT_1:def 4; :: thesis: verum