:: deftheorem defines omf REALSET2:def 5 :
for F being non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr holds omf F = the multF of F;