let A, B be set ; :: thesis: for D being non empty set
for f being BinOp of D st A c= B & f is B -one-to-one holds
f is A -one-to-one
let D be non empty set ; :: thesis: for f being BinOp of D st A c= B & f is B -one-to-one holds
f is A -one-to-one
let f be BinOp of D; :: thesis: ( A c= B & f is B -one-to-one implies f is A -one-to-one )
assume ( A c= B & f is B -one-to-one ) ; :: thesis: f is A -one-to-one
then ( f | B is one-to-one & f | A = (f | B) | A ) by FUNCT_1:51;
hence f is A -one-to-one by FUNCT_1:52; :: thesis: verum