theorem Th10: :: BKMODEL4:19

for a11, a12, a13, a21, a22, a23, a31, a32, a33, b11, b12, b13, b21, b22, b23, b31, b32, b33, ab11, ab12, ab13, ab21, ab22, ab23, ab31, ab32, ab33 being Element of F_Real
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*>*> & ab11 = ((a11 * b11) + (a12 * b21)) + (a13 * b31) & ab12 = ((a11 * b12) + (a12 * b22)) + (a13 * b32) & ab13 = ((a11 * b13) + (a12 * b23)) + (a13 * b33) & ab21 = ((a21 * b11) + (a22 * b21)) + (a23 * b31) & ab22 = ((a21 * b12) + (a22 * b22)) + (a23 * b32) & ab23 = ((a21 * b13) + (a22 * b23)) + (a23 * b33) & ab31 = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & ab32 = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & ab33 = ((a31 * b13) + (a32 * b23)) + (a33 * b33) holds
A * B = <*<*ab11,ab12,ab13*>,<*ab21,ab22,ab23*>,<*ab31,ab32,ab33*>*> by ANPROJ_9:6;