let a11, a12, a13, a21, a22, a23, a31, a32, a33, b1, b2, b3 be Element of F_Real; :: thesis: for A being Matrix of 3,3,F_Real
for B being Matrix of 3,1,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> & B = <*<*b1*>,<*b2*>,<*b3*>*> holds
A * B = <*<*(((a11 * b1) + (a12 * b2)) + (a13 * b3))*>,<*(((a21 * b1) + (a22 * b2)) + (a23 * b3))*>,<*(((a31 * b1) + (a32 * b2)) + (a33 * b3))*>*>
let A be Matrix of 3,3,F_Real; :: thesis: for B being Matrix of 3,1,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> & B = <*<*b1*>,<*b2*>,<*b3*>*> holds
A * B = <*<*(((a11 * b1) + (a12 * b2)) + (a13 * b3))*>,<*(((a21 * b1) + (a22 * b2)) + (a23 * b3))*>,<*(((a31 * b1) + (a32 * b2)) + (a33 * b3))*>*>
let B be Matrix of 3,1,F_Real; :: thesis: ( A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> & B = <*<*b1*>,<*b2*>,<*b3*>*> implies A * B = <*<*(((a11 * b1) + (a12 * b2)) + (a13 * b3))*>,<*(((a21 * b1) + (a22 * b2)) + (a23 * b3))*>,<*(((a31 * b1) + (a32 * b2)) + (a33 * b3))*>*> )
assume that
A1: A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> and
A2: B = <*<*b1*>,<*b2*>,<*b3*>*> ; :: thesis: A * B = <*<*(((a11 * b1) + (a12 * b2)) + (a13 * b3))*>,<*(((a21 * b1) + (a22 * b2)) + (a23 * b3))*>,<*(((a31 * b1) + (a32 * b2)) + (a33 * b3))*>*>
A3: ( width A = 3 & len B = 3 & len A = 3 & width B = 1 ) by MATRIX_0:23;
A4: ( len (A * B) = 3 & width (A * B) = 1 ) by A3, MATRIX_3:def 4;
A5: A * B is Matrix of 3,1,F_Real by A4, MATRIX_0:20;
then A6: ( [1,1] in Indices (A * B) & [2,1] in Indices (A * B) & [3,1] in Indices (A * B) ) by ANPROJ_8:2, MATRIX_0:23;
A7: ( Line (A,1) = <*a11,a12,a13*> & Line (A,2) = <*a21,a22,a23*> & Line (A,3) = <*a31,a32,a33*> ) by A1, Th05;
( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
then A8: ( 1 in dom B & 2 in dom B & 3 in dom B ) by FINSEQ_1:def 3, A3;

now :: thesis: ( len (Col (B,1)) = 3 & (Col (B,1)) . 1 = b1 & (Col (B,1)) . 2 = b2 & (Col (B,1)) . 3 = b3 )

thus len (Col (B,1)) = 3 by A3, MATRIX_0:def 8; :: thesis: ( (Col (B,1)) . 1 = b1 & (Col (B,1)) . 2 = b2 & (Col (B,1)) . 3 = b3 )
[1,1] in Indices B by MATRIX_0:23, ANPROJ_8:2;
then consider p being FinSequence of F_Real such that
A9: p = B . 1 and
A10: B * (1,1) = p . 1 by MATRIX_0:def 5;
B * (1,1) = <*b1*> . 1 by A9, A10, A2
.= b1 ;
hence (Col (B,1)) . 1 = b1 by A8, MATRIX_0:def 8; :: thesis: ( (Col (B,1)) . 2 = b2 & (Col (B,1)) . 3 = b3 )
[2,1] in Indices B by MATRIX_0:23, ANPROJ_8:2;
then consider p being FinSequence of F_Real such that
A11: p = B . 2 and
A12: B * (2,1) = p . 1 by MATRIX_0:def 5;
B * (2,1) = <*b2*> . 1 by A11, A12, A2
.= b2 ;
hence (Col (B,1)) . 2 = b2 by A8, MATRIX_0:def 8; :: thesis: (Col (B,1)) . 3 = b3
[3,1] in Indices B by MATRIX_0:23, ANPROJ_8:2;
then consider p being FinSequence of F_Real such that
A13: p = B . 3 and
A14: B * (3,1) = p . 1 by MATRIX_0:def 5;
B * (3,1) = <*b3*> . 1 by A13, A14, A2
.= b3 ;
hence (Col (B,1)) . 3 = b3 by A8, MATRIX_0:def 8; :: thesis: verum

end;

then A15: Col (B,1) = <*b1,b2,b3*> by FINSEQ_1:45;

now :: thesis: ( (A * B) * (1,1) = ((a11 * b1) + (a12 * b2)) + (a13 * b3) & (A * B) * (2,1) = ((a21 * b1) + (a22 * b2)) + (a23 * b3) & (A * B) * (3,1) = ((a31 * b1) + (a32 * b2)) + (a33 * b3) )

thus (A * B) * (1,1) = (Line (A,1)) "*" (Col (B,1)) by A3, A6, MATRIX_3:def 4
.= ((a11 * b1) + (a12 * b2)) + (a13 * b3) by A7, A15, ANPROJ_8:7 ; :: thesis: ( (A * B) * (2,1) = ((a21 * b1) + (a22 * b2)) + (a23 * b3) & (A * B) * (3,1) = ((a31 * b1) + (a32 * b2)) + (a33 * b3) )
thus (A * B) * (2,1) = (Line (A,2)) "*" (Col (B,1)) by A3, A6, MATRIX_3:def 4
.= ((a21 * b1) + (a22 * b2)) + (a23 * b3) by A7, A15, ANPROJ_8:7 ; :: thesis: (A * B) * (3,1) = ((a31 * b1) + (a32 * b2)) + (a33 * b3)
thus (A * B) * (3,1) = (Line (A,3)) "*" (Col (B,1)) by A3, A6, MATRIX_3:def 4
.= ((a31 * b1) + (a32 * b2)) + (a33 * b3) by A7, A15, ANPROJ_8:7 ; :: thesis: verum

end;

then A16: ( Line ((A * B),1) = <*(((a11 * b1) + (a12 * b2)) + (a13 * b3))*> & Line ((A * B),2) = <*(((a21 * b1) + (a22 * b2)) + (a23 * b3))*> & Line ((A * B),3) = <*(((a31 * b1) + (a32 * b2)) + (a33 * b3))*> ) by A5, ANPROJ_8:90;

now :: thesis: ( len (A * B) = 3 & (A * B) . 1 = Line ((A * B),1) & (A * B) . 2 = Line ((A * B),2) & (A * B) . 3 = Line ((A * B),3) )

thus len (A * B) = 3 by A3, MATRIX_3:def 4; :: thesis: ( (A * B) . 1 = Line ((A * B),1) & (A * B) . 2 = Line ((A * B),2) & (A * B) . 3 = Line ((A * B),3) )
( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
hence ( (A * B) . 1 = Line ((A * B),1) & (A * B) . 2 = Line ((A * B),2) & (A * B) . 3 = Line ((A * B),3) ) by A5, MATRIX_0:52; :: thesis: verum

end;

hence A * B = <*<*(((a11 * b1) + (a12 * b2)) + (a13 * b3))*>,<*(((a21 * b1) + (a22 * b2)) + (a23 * b3))*>,<*(((a31 * b1) + (a32 * b2)) + (a33 * b3))*>*> by A16, FINSEQ_1:45; :: thesis: verum