let r, a, b, c, d, e, f, g, h, i be Element of F_Real; :: thesis: for M being Matrix of 3,F_Real st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
r * M = <*<*(r * a),(r * b),(r * c)*>,<*(r * d),(r * e),(r * f)*>,<*(r * g),(r * h),(r * i)*>*>
let M be Matrix of 3,F_Real; :: thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies r * M = <*<*(r * a),(r * b),(r * c)*>,<*(r * d),(r * e),(r * f)*>,<*(r * g),(r * h),(r * i)*>*> )
assume A1: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; :: thesis: r * M = <*<*(r * a),(r * b),(r * c)*>,<*(r * d),(r * e),(r * f)*>,<*(r * g),(r * h),(r * i)*>*>
( len M = 3 & width M = 3 ) by MATRIX_0:23;
then ( len (r * M) = 3 & width (r * M) = 3 ) by MATRIX_3:def 5;
then A2: r * M is Matrix of 3,3,F_Real by MATRIX_0:20;
A3: Indices M = [:(Seg 3),(Seg 3):] by MATRIX_0:23;
reconsider b11 = (r * M) * (1,1), b12 = (r * M) * (1,2), b13 = (r * M) * (1,3), b21 = (r * M) * (2,1), b22 = (r * M) * (2,2), b23 = (r * M) * (2,3), b31 = (r * M) * (3,1), b32 = (r * M) * (3,2), b33 = (r * M) * (3,3) as Element of F_Real ;
M = <*<*(M * (1,1)),(M * (1,2)),(M * (1,3))*>,<*(M * (2,1)),(M * (2,2)),(M * (2,3))*>,<*(M * (3,1)),(M * (3,2)),(M * (3,3))*>*> by MATRIXR2:37;
then A4: ( a = M * (1,1) & b = M * (1,2) & c = M * (1,3) & d = M * (2,1) & e = M * (2,2) & f = M * (2,3) & g = M * (3,1) & h = M * (3,2) & i = M * (3,3) ) by A1, PASCAL:2;
( b11 = r * (M * (1,1)) & b12 = r * (M * (1,2)) & b13 = r * (M * (1,3)) & b21 = r * (M * (2,1)) & b22 = r * (M * (2,2)) & b23 = r * (M * (2,3)) & b31 = r * (M * (3,1)) & b32 = r * (M * (3,2)) & b33 = r * (M * (3,3)) ) by A3, ANPROJ_8:1, MATRIX_3:def 5;
hence r * M = <*<*(r * a),(r * b),(r * c)*>,<*(r * d),(r * e),(r * f)*>,<*(r * g),(r * h),(r * i)*>*> by A4, A2, MATRIXR2:37; :: thesis: verum