let f be Function; :: thesis: for X, Y being set st X c= Y & f | Y is one-to-one holds
f | X is one-to-one
let X, Y be set ; :: thesis: ( X c= Y & f | Y is one-to-one implies f | X is one-to-one )
assume that
A1: X c= Y and
A2: f | Y is one-to-one ; :: thesis: f | X is one-to-one
f | X = (f | Y) | X by A1, RELAT_1:74;
hence f | X is one-to-one by A2, FUNCT_1:52; :: thesis: verum