:: deftheorem Def01 defines (*) ANPROJ_9:def 2 :
for h1, h2, b₃ being Element of EnsHomography3 holds
( b₃ = h1 (*) h2 iff ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = homography N1 & h2 = homography N2 & b₃ = homography (N1 * N2) ) );