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
let x, y be object ; :: according to FUNCT_1:def 4 :: 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 )
A3: dom (f | Y) = (dom f) /\ Y by RELAT_1:61;
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;
x in dom f by A3, A4, XBOOLE_0:def 4;
then x in (dom f) /\ X by A2, A5, XBOOLE_0:def 4;
then A6: x in dom (f | X) by RELAT_1:61;
assume A7: y in dom (f | Y) ; :: thesis: ( not (f | Y) . x = (f | Y) . y or x = y )
then A8: y in Y by A3, XBOOLE_0:def 4;
y in dom f by A3, A7, XBOOLE_0:def 4;
then y in (dom f) /\ X by A2, A8, XBOOLE_0:def 4;
then A9: y in dom (f | X) by RELAT_1:61;
assume A10: (f | Y) . x = (f | Y) . y ; :: thesis: x = y
(f | X) . x = f . x by A2, A5, FUNCT_1:49
.= (f | Y) . x by A5, FUNCT_1:49
.= f . y by A8, A10, FUNCT_1:49
.= (f | X) . y by A2, A8, FUNCT_1:49 ;
hence x = y by A1, A6, A9; :: thesis: verum