let A, B be set ; :: thesis: for D being non empty set
for f being BinOp of D st B is f -unambiguous & A c= B holds
A is f -unambiguous
let D be non empty set ; :: thesis: for f being BinOp of D st B is f -unambiguous & A c= B holds
A is f -unambiguous
let f be BinOp of D; :: thesis: ( B is f -unambiguous & A c= B implies A is f -unambiguous )
assume A0: ( B is f -unambiguous & A c= B ) ; :: thesis: A is f -unambiguous
then [:A,D:] c= [:B,D:] by ZFMISC_1:95;
then f is [:A,D:] -one-to-one by A0, Lm4;
hence A is f -unambiguous ; :: thesis: verum