let X be set ; :: thesis: for n being natural number holds canon_image X,n is one-to-one
let n be natural number ; :: thesis: canon_image X,n is one-to-one
for x1, x2 being set 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 set ; :: 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, Def20;
hence x1 = x2 by A2, ZFMISC_1:33; :: thesis: verum

end;

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

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

end;

end;

end;

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