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;

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 )

then A15:
Col (B,1) = <*b1,b2,b3*>
by FINSEQ_1:45;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, FINSEQ_1:45

.= b1 by FINSEQ_1:def 8 ;

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, FINSEQ_1:45

.= b2 by FINSEQ_1:def 8 ;

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, FINSEQ_1:45

.= b3 by FINSEQ_1:def 8 ;

hence (Col (B,1)) . 3 = b3 by A8, MATRIX_0:def 8; :: thesis: verum

end;[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, FINSEQ_1:45

.= b1 by FINSEQ_1:def 8 ;

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, FINSEQ_1:45

.= b2 by FINSEQ_1:def 8 ;

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, FINSEQ_1:45

.= b3 by FINSEQ_1:def 8 ;

hence (Col (B,1)) . 3 = b3 by A8, MATRIX_0:def 8; :: thesis: verum

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) )

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;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;.= ((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

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) )

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: verumthus
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;( 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