:: deftheorem defines GroupHomography3 ANPROJ_9:def 4 :
GroupHomography3 = multMagma(# EnsHomography3,BinOpHomography3 #);