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 = <*(((a11 * b11) + (a12 * b21)) + (a13 * b31)),(((a11 * b12) + (a12 * b22)) + (a13 * b32)),(((a11 * b13) + (a12 * b23)) + (a13 * b33))*> & (A * B) . 2 = <*(((a21 * b11) + (a22 * b21)) + (a23 * b31)),(((a21 * b12) + (a22 * b22)) + (a23 * b32)),(((a21 * b13) + (a22 * b23)) + (a23 * b33))*> & (A * B) . 3 = <*(((a31 * b11) + (a32 * b21)) + (a33 * b31)),(((a31 * b12) + (a32 * b22)) + (a33 * b32)),(((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 = <*(((a11 * b11) + (a12 * b21)) + (a13 * b31)),(((a11 * b12) + (a12 * b22)) + (a13 * b32)),(((a11 * b13) + (a12 * b23)) + (a13 * b33))*> & (A * B) . 2 = <*(((a21 * b11) + (a22 * b21)) + (a23 * b31)),(((a21 * b12) + (a22 * b22)) + (a23 * b32)),(((a21 * b13) + (a22 * b23)) + (a23 * b33))*> & (A * B) . 3 = <*(((a31 * b11) + (a32 * b21)) + (a33 * b31)),(((a31 * b12) + (a32 * b22)) + (a33 * b32)),(((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 = <*(((a11 * b11) + (a12 * b21)) + (a13 * b31)),(((a11 * b12) + (a12 * b22)) + (a13 * b32)),(((a11 * b13) + (a12 * b23)) + (a13 * b33))*> & (A * B) . 2 = <*(((a21 * b11) + (a22 * b21)) + (a23 * b31)),(((a21 * b12) + (a22 * b22)) + (a23 * b32)),(((a21 * b13) + (a22 * b23)) + (a23 * b33))*> & (A * B) . 3 = <*(((a31 * b11) + (a32 * b21)) + (a33 * b31)),(((a31 * b12) + (a32 * b22)) + (a33 * b32)),(((a31 * b13) + (a32 * b23)) + (a33 * b33))*> )

now :: thesis: ( len (A * B) = 3 & 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))*>*> )

now :: thesis: ( len A = 3 & len (A * B) = len A )

thus len A = 3 by A1, FINSEQ_1:45; :: thesis: len (A * B) = len A
( width A = 3 & len B = 3 ) by MATRIX_0:23;
hence len (A * B) = len A by MATRIX_3:def 4; :: thesis: verum

end;

hence len (A * B) = 3 ; :: thesis: 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))*>*>
thus 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, Th07; :: thesis: verum

end;

hence ( (A * B) . 1 = <*(((a11 * b11) + (a12 * b21)) + (a13 * b31)),(((a11 * b12) + (a12 * b22)) + (a13 * b32)),(((a11 * b13) + (a12 * b23)) + (a13 * b33))*> & (A * B) . 2 = <*(((a21 * b11) + (a22 * b21)) + (a23 * b31)),(((a21 * b12) + (a22 * b22)) + (a23 * b32)),(((a21 * b13) + (a22 * b23)) + (a23 * b33))*> & (A * B) . 3 = <*(((a31 * b11) + (a32 * b21)) + (a33 * b31)),(((a31 * b12) + (a32 * b22)) + (a33 * b32)),(((a31 * b13) + (a32 * b23)) + (a33 * b33))*> ) ; :: thesis: verum