let p1, p2, p3, q1, q2, q3, r1, r2, r3 be Real; :: thesis: <*<*p1,p2,p3*>,<*q1,q2,q3*>,<*r1,r2,r3*>*> is Matrix of 3,F_Real
reconsider P1 = p1, P2 = p2, P3 = p3, Q1 = q1, Q2 = q2, Q3 = q3, R1 = r1, R2 = r2, R3 = r3 as Element of F_Real by XREAL_0:def 1;
<*<*P1,P2,P3*>,<*Q1,Q2,Q3*>,<*R1,R2,R3*>*> is Matrix of 3,F_Real by MATRIXR2:35;
hence <*<*p1,p2,p3*>,<*q1,q2,q3*>,<*r1,r2,r3*>*> is Matrix of 3,F_Real ; :: thesis: verum