let D be non empty set ; :: thesis: for B, A being set
for f being BinOp of D st B is f -unambiguous & A c= B holds
A is f -unambiguous
let B, A be 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 ( B is f -unambiguous & A c= B ) ; :: thesis: A is f -unambiguous
then C1: ( f is [:B,D:] -one-to-one & A c= B ) by DefUnambiguous1;
f is [:A,D:] -one-to-one by C1, Lm12, ZFMISC_1:96;
hence A is f -unambiguous by DefUnambiguous1; :: thesis: verum