theorem Th16: :: ANPROJ_8:19

for p1, p2, p3, q1, q2, q3, r1, r2, r3 being Real holds <*<*p1,p2,p3*>,<*q1,q2,q3*>,<*r1,r2,r3*>*> is Matrix of 3,F_Real