theorem Ta1: :: ANPROJ_9:19

for x, y, z being Element of EnsHomography3 holds (x (*) y) (*) z = x (*) (y (*) z)