theorem Th17: :: ANPROJ_8:20

for M being Matrix of 3,F_Real
for p1, p2, p3, q1, q2, q3, r1, r2, r3 being Real st M = <*<*p1,q1,r1*>,<*p2,q2,r2*>,<*p3,q3,r3*>*> holds
( M * (1,1) = p1 & M * (1,2) = q1 & M * (1,3) = r1 & M * (2,1) = p2 & M * (2,2) = q2 & M * (2,3) = r2 & M * (3,1) = p3 & M * (3,2) = q3 & M * (3,3) = r3 )