let f be Function; :: thesis: for X, Y being set st f | X is one-to-one & Y c= X holds
f | Y is one-to-one
let X, Y be set ; :: thesis: ( f | X is one-to-one & Y c= X implies f | Y is one-to-one )
assume that
A1: f | X is one-to-one and
A2: Y c= X ; :: thesis: f | Y is one-to-one
A3: dom (f | Y) = (dom f) /\ Y by RELAT_1:90;
let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in dom (f | Y) or not y in dom (f | Y) or not (f | Y) . x = (f | Y) . y or x = y )
assume A4: x in dom (f | Y) ; :: thesis: ( not y in dom (f | Y) or not (f | Y) . x = (f | Y) . y or x = y )
then A5: x in Y by A3, XBOOLE_0:def 4;
assume A6: y in dom (f | Y) ; :: thesis: ( not (f | Y) . x = (f | Y) . y or x = y )
then A7: y in Y by A3, XBOOLE_0:def 4;
assume A8: (f | Y) . x = (f | Y) . y ; :: thesis: x = y
A9: (f | X) . x = f . x by A2, A5, FUNCT_1:72
.= (f | Y) . x by A5, FUNCT_1:72
.= f . y by A7, A8, FUNCT_1:72
.= (f | X) . y by A2, A7, FUNCT_1:72 ;
( x in dom f & y in dom f ) by A3, A4, A6, XBOOLE_0:def 4;
then ( x in (dom f) /\ X & y in (dom f) /\ X ) by A2, A5, A7, XBOOLE_0:def 4;
then ( x in dom (f | X) & y in dom (f | X) ) by RELAT_1:90;
hence x = y by A1, A9, FUNCT_1:def 8; :: thesis: verum