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 ;
A5: A * B is Matrix of 3,1,F_Real by ;
then A6: ( [1,1] in Indices (A * B) & [2,1] in Indices (A * B) & [3,1] in Indices (A * B) ) by ;
A7: ( Line (A,1) = <*a11,a12,a13*> & Line (A,2) = <*a21,a22,a23*> & Line (A,3) = <*a31,a32,a33*> ) by ;
( 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 ;
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 ; :: thesis: ( (Col (B,1)) . 1 = b1 & (Col (B,1)) . 2 = b2 & (Col (B,1)) . 3 = b3 )
[1,1] in Indices B by ;
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
.= b1 by FINSEQ_1:def 8 ;
hence (Col (B,1)) . 1 = b1 by ; :: thesis: ( (Col (B,1)) . 2 = b2 & (Col (B,1)) . 3 = b3 )
[2,1] in Indices B by ;
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
.= b2 by FINSEQ_1:def 8 ;
hence (Col (B,1)) . 2 = b2 by ; :: thesis: (Col (B,1)) . 3 = b3
[3,1] in Indices B by ;
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
.= b3 by FINSEQ_1:def 8 ;
hence (Col (B,1)) . 3 = b3 by ; :: 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
.= ((a11 * b1) + (a12 * b2)) + (a13 * b3) by ; :: 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
.= ((a21 * b1) + (a22 * b2)) + (a23 * b3) by ; :: thesis: (A * B) * (3,1) = ((a31 * b1) + (a32 * b2)) + (a33 * b3)
thus (A * B) * (3,1) = (Line (A,3)) "*" (Col (B,1)) by
.= ((a31 * b1) + (a32 * b2)) + (a33 * b3) by ; :: 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 ;
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 ; :: 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 ; :: 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 ; :: thesis: verum