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

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