let M be Matrix of 3,F_Real; :: thesis: 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 @ = <*<*p1,p2,p3*>,<*q1,q2,q3*>,<*r1,r2,r3*>*>
let p1, p2, p3, q1, q2, q3, r1, r2, r3 be Real; :: thesis: ( M = <*<*p1,q1,r1*>,<*p2,q2,r2*>,<*p3,q3,r3*>*> implies M @ = <*<*p1,p2,p3*>,<*q1,q2,q3*>,<*r1,r2,r3*>*> )
assume A1: M = <*<*p1,q1,r1*>,<*p2,q2,r2*>,<*p3,q3,r3*>*> ; :: thesis: M @ = <*<*p1,p2,p3*>,<*q1,q2,q3*>,<*r1,r2,r3*>*>
Indices M = [:(Seg 3),(Seg 3):] by MATRIX_0:24;
then A2: ( (M @) * (1,1) = M * (1,1) & (M @) * (1,2) = M * (2,1) & (M @) * (1,3) = M * (3,1) & (M @) * (2,1) = M * (1,2) & (M @) * (2,2) = M * (2,2) & (M @) * (2,3) = M * (3,2) & (M @) * (3,1) = M * (1,3) & (M @) * (3,2) = M * (2,3) & (M @) * (3,3) = M * (3,3) ) by MATRIX_0:def 6, Th1;
( M * (1,1) = p1 & M * (2,1) = p2 & M * (3,1) = p3 & M * (1,2) = q1 & M * (2,2) = q2 & M * (3,2) = q3 & M * (1,3) = r1 & M * (2,3) = r2 & M * (3,3) = r3 ) by A1, Th17;
hence M @ = <*<*p1,p2,p3*>,<*q1,q2,q3*>,<*r1,r2,r3*>*> by A2, MATRIXR2:37; :: thesis: verum