:: deftheorem defines GroupLineHomography3 BKMODEL3:def 6 :
GroupLineHomography3 = multMagma(# EnsLineHomography3,BinOpLineHomography3 #);