let x be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st width A = len x & len x > 0 & len A > 0 holds
A * (ColVec2Mx x) = ColVec2Mx (A * x)
let A be Matrix of REAL ; :: thesis: ( width A = len x & len x > 0 & len A > 0 implies A * (ColVec2Mx x) = ColVec2Mx (A * x) )
assume A1: ( width A = len x & len x > 0 & len A > 0 ) ; :: thesis: A * (ColVec2Mx x) = ColVec2Mx (A * x)
then A2: len (A * x) = len A by MATRIXR1:61;
then A3: ( len (ColVec2Mx (A * x)) = len (A * x) & width (ColVec2Mx (A * x)) = 1 ) by A1, MATRIXR1:def 9;
A4: ( len (ColVec2Mx x) = len x & width (ColVec2Mx x) = 1 ) by A1, MATRIXR1:def 9;
then A5: ( len (ColVec2Mx (A * x)) = len A & width (ColVec2Mx (A * x)) = width (ColVec2Mx x) ) by A1, A2, MATRIXR1:def 9;
A6: len (MXR2MXF (ColVec2Mx (A * x))) = len (MXR2MXF A) by A1, A2, MATRIXR1:def 9;
A7: width (MXR2MXF (ColVec2Mx (A * x))) = 1 by A1, A2, MATRIXR1:def 9
.= width (MXR2MXF (ColVec2Mx x)) by A1, MATRIXR1:def 9 ;
A8: len (MXR2MXF (ColVec2Mx x)) = width (MXR2MXF A) by A1, MATRIXR1:def 9;
then A9: len ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))) = len A by MATRIX_3:def 4;
A10: width ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))) = width (ColVec2Mx x) by A8, MATRIX_3:def 4
.= 1 by A1, MATRIXR1:def 9 ;
for i, j being Nat st [i,j] in Indices (MXR2MXF (ColVec2Mx (A * x))) holds
(MXR2MXF (ColVec2Mx (A * x))) * i,j = (Line (MXR2MXF A),i) "*" (Col (MXR2MXF (ColVec2Mx x)),j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (MXR2MXF (ColVec2Mx (A * x))) implies (MXR2MXF (ColVec2Mx (A * x))) * i,j = (Line (MXR2MXF A),i) "*" (Col (MXR2MXF (ColVec2Mx x)),j) )
assume A11: [i,j] in Indices (MXR2MXF (ColVec2Mx (A * x))) ; :: thesis: (MXR2MXF (ColVec2Mx (A * x))) * i,j = (Line (MXR2MXF A),i) "*" (Col (MXR2MXF (ColVec2Mx x)),j)
A12: Indices (ColVec2Mx (A * x)) = [:(Seg (len A)),(Seg 1):] by A2, A3, FINSEQ_1:def 3;
then A13: ( j in Seg 1 & i in Seg (len A) ) by A11, ZFMISC_1:106;
then ( 1 <= j & j <= 1 ) by FINSEQ_1:3;
then A14: j = 1 by XXREAL_0:1;
A15: i in dom (A * x) by A2, A13, FINSEQ_1:def 3;
A16: ( i in Seg (len (ColVec2Mx (A * x))) & 1 in Seg 1 ) by A5, A11, A12, ZFMISC_1:106;
Indices (ColVec2Mx (A * x)) = [:(Seg (len (ColVec2Mx (A * x)))),(Seg 1):] by A3, FINSEQ_1:def 3;
then [i,1] in Indices (ColVec2Mx (A * x)) by A16, ZFMISC_1:106;
then consider p2 being FinSequence of REAL such that
A17: ( p2 = (ColVec2Mx (A * x)) . i & (ColVec2Mx (A * x)) * i,1 = p2 . 1 ) by MATRIX_1:def 6;
A18: (Col (A * (ColVec2Mx x)),1) . i = <*((A * x) . i)*> . 1 by FINSEQ_1:57
.= (ColVec2Mx (A * x)) * i,1 by A1, A2, A15, A17, MATRIXR1:def 9 ;
len (A * (ColVec2Mx x)) = len A by A1, A4, MATRIX_3:def 4;
then i in dom (A * (ColVec2Mx x)) by A13, FINSEQ_1:def 3;
then A19: (Col (A * (ColVec2Mx x)),1) . i = (A * (ColVec2Mx x)) * i,j by A14, MATRIX_1:def 9;
A20: i in Seg (len ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x)))) by A9, A11, A12, ZFMISC_1:106;
j in Seg (width ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x)))) by A3, A10, A11, ZFMISC_1:106;
then [i,j] in [:(Seg (len ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))))),(Seg (width ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))))):] by A20, ZFMISC_1:106;
then [i,j] in Indices ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))) by FINSEQ_1:def 3;
hence (MXR2MXF (ColVec2Mx (A * x))) * i,j = (Line (MXR2MXF A),i) "*" (Col (MXR2MXF (ColVec2Mx x)),j) by A8, A14, A18, A19, MATRIX_3:def 4; :: thesis: verum

end;

hence A * (ColVec2Mx x) = ColVec2Mx (A * x) by A6, A7, A8, MATRIX_3:def 4; :: thesis: verum