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 set ; :: according to FUNCT_1:def 4 :: thesis: for x2 being set st x1 in dom (Y | f) & x2 in dom (Y | f) & (Y | f) . x1 = (Y | f) . x2 holds
x1 = x2
let x2 be set ; :: 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, Th85;
( (Y | f) . x1 = f . x1 & (Y | f) . x2 = f . x2 ) by A2, Th85;
hence x1 = x2 by A1, A3, A4, Def8; :: thesis: verum