let Y be set ; :: thesis: for f being Function st f is one-to-one holds
Y |` f is one-to-one
let f be Function; :: thesis: ( f is one-to-one implies Y |` f is one-to-one )
assume A1: f is one-to-one ; :: thesis: Y |` f is one-to-one
let x1 be object ; :: according to FUNCT_1:def 4 :: thesis: for x2 being object st x1 in dom (Y |` f) & x2 in dom (Y |` f) & (Y |` f) . x1 = (Y |` f) . x2 holds
x1 = x2
let x2 be object ; :: thesis: ( x1 in dom (Y |` f) & x2 in dom (Y |` f) & (Y |` f) . x1 = (Y |` f) . x2 implies x1 = x2 )
assume that
A2: ( x1 in dom (Y |` f) & x2 in dom (Y |` f) ) and
A3: (Y |` f) . x1 = (Y |` f) . x2 ; :: thesis: x1 = x2
A4: ( x1 in dom f & x2 in dom f ) by A2, Th52;
( (Y |` f) . x1 = f . x1 & (Y |` f) . x2 = f . x2 ) by A2, Th52;
hence x1 = x2 by A1, A3, A4; :: thesis: verum