:: deftheorem Def02 defines BinOpHomography3 ANPROJ_9:def 3 :
for b₁ being BinOp of EnsHomography3 holds
( b₁ = BinOpHomography3 iff for h1, h2 being Element of EnsHomography3 holds b₁ . (h1,h2) = h1 (*) h2 );