let a11, a12, a13, a21, a22, a23, a31, a32, a33, b11, b12, b13, b21, b22, b23, b31, b32, b33 be Element of F_Real; :: thesis: for A, B being Matrix of 3,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> & B = <*<*b11,b12,b13*>,<*b21,b22,b23*>,<*b31,b32,b33*>*> holds
( (A * B) * (1,1) = ((a11 * b11) + (a12 * b21)) + (a13 * b31) & (A * B) * (1,2) = ((a11 * b12) + (a12 * b22)) + (a13 * b32) & (A * B) * (1,3) = ((a11 * b13) + (a12 * b23)) + (a13 * b33) & (A * B) * (2,1) = ((a21 * b11) + (a22 * b21)) + (a23 * b31) & (A * B) * (2,2) = ((a21 * b12) + (a22 * b22)) + (a23 * b32) & (A * B) * (2,3) = ((a21 * b13) + (a22 * b23)) + (a23 * b33) & (A * B) * (3,1) = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & (A * B) * (3,2) = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & (A * B) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33) )
let A, B be Matrix of 3,F_Real; :: thesis: ( A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> & B = <*<*b11,b12,b13*>,<*b21,b22,b23*>,<*b31,b32,b33*>*> implies ( (A * B) * (1,1) = ((a11 * b11) + (a12 * b21)) + (a13 * b31) & (A * B) * (1,2) = ((a11 * b12) + (a12 * b22)) + (a13 * b32) & (A * B) * (1,3) = ((a11 * b13) + (a12 * b23)) + (a13 * b33) & (A * B) * (2,1) = ((a21 * b11) + (a22 * b21)) + (a23 * b31) & (A * B) * (2,2) = ((a21 * b12) + (a22 * b22)) + (a23 * b32) & (A * B) * (2,3) = ((a21 * b13) + (a22 * b23)) + (a23 * b33) & (A * B) * (3,1) = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & (A * B) * (3,2) = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & (A * B) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33) ) )
assume that
A1: A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> and
A2: B = <*<*b11,b12,b13*>,<*b21,b22,b23*>,<*b31,b32,b33*>*> ; :: thesis: ( (A * B) * (1,1) = ((a11 * b11) + (a12 * b21)) + (a13 * b31) & (A * B) * (1,2) = ((a11 * b12) + (a12 * b22)) + (a13 * b32) & (A * B) * (1,3) = ((a11 * b13) + (a12 * b23)) + (a13 * b33) & (A * B) * (2,1) = ((a21 * b11) + (a22 * b21)) + (a23 * b31) & (A * B) * (2,2) = ((a21 * b12) + (a22 * b22)) + (a23 * b32) & (A * B) * (2,3) = ((a21 * b13) + (a22 * b23)) + (a23 * b33) & (A * B) * (3,1) = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & (A * B) * (3,2) = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & (A * B) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33) )
A3: A * B = <*<*(((a11 * b11) + (a12 * b21)) + (a13 * b31)),(((a11 * b12) + (a12 * b22)) + (a13 * b32)),(((a11 * b13) + (a12 * b23)) + (a13 * b33))*>,<*(((a21 * b11) + (a22 * b21)) + (a23 * b31)),(((a21 * b12) + (a22 * b22)) + (a23 * b32)),(((a21 * b13) + (a22 * b23)) + (a23 * b33))*>,<*(((a31 * b11) + (a32 * b21)) + (a33 * b31)),(((a31 * b12) + (a32 * b22)) + (a33 * b32)),(((a31 * b13) + (a32 * b23)) + (a33 * b33))*>*> by A1, A2, ANPROJ_9:6;
reconsider C = A * B as Matrix of 3,F_Real ;
C = <*<*(C * (1,1)),(C * (1,2)),(C * (1,3))*>,<*(C * (2,1)),(C * (2,2)),(C * (2,3))*>,<*(C * (3,1)),(C * (3,2)),(C * (3,3))*>*> by MATRIXR2:37;
hence ( (A * B) * (1,1) = ((a11 * b11) + (a12 * b21)) + (a13 * b31) & (A * B) * (1,2) = ((a11 * b12) + (a12 * b22)) + (a13 * b32) & (A * B) * (1,3) = ((a11 * b13) + (a12 * b23)) + (a13 * b33) & (A * B) * (2,1) = ((a21 * b11) + (a22 * b21)) + (a23 * b31) & (A * B) * (2,2) = ((a21 * b12) + (a22 * b22)) + (a23 * b32) & (A * B) * (2,3) = ((a21 * b13) + (a22 * b23)) + (a23 * b33) & (A * B) * (3,1) = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & (A * B) * (3,2) = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & (A * B) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33) ) by A3, PASCAL:2; :: thesis: verum