:: deftheorem Def00 defines 00-dominant FUZIMPL1:def 3 :
for f being BinOp of [.0,1.] holds
( f is 00-dominant iff f . (0,0) = 1 );