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 that
A1: width A = len x and
A2: len x > 0 and
A3: len A > 0 ; :: thesis: A * (ColVec2Mx x) = ColVec2Mx (A * x)
A4: len (ColVec2Mx x) = len x by A2, MATRIXR1:def 9;
A5: len (MXR2MXF (ColVec2Mx x)) = width (MXR2MXF A) by A1, A2, MATRIXR1:def 9;
then A6: width ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))) = width (ColVec2Mx x) by MATRIX_3:def 4
.= 1 by A2, MATRIXR1:def 9 ;
A7: len ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))) = len A by A5, MATRIX_3:def 4;
A8: len (A * x) = len A by A1, A2, MATRIXR1:61;
then A9: width (ColVec2Mx (A * x)) = 1 by A3, MATRIXR1:def 9;
A10: len (ColVec2Mx (A * x)) = len A by A3, A8, MATRIXR1:def 9;
A11: len (ColVec2Mx (A * x)) = len (A * x) by A3, A8, MATRIXR1:def 9;
A12: 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)) )
A13: ( 1 in Seg 1 & Indices (ColVec2Mx (A * x)) = [:(Seg (len (ColVec2Mx (A * x)))),(Seg 1):] ) by A9, FINSEQ_1:def 3;
assume A14: [i,j] in Indices (MXR2MXF (ColVec2Mx (A * x))) ; :: thesis: (MXR2MXF (ColVec2Mx (A * x))) * (i,j) = (Line ((MXR2MXF A),i)) "*" (Col ((MXR2MXF (ColVec2Mx x)),j))
then A15: j in Seg (width ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x)))) by A9, A6, ZFMISC_1:87;
A16: Indices (ColVec2Mx (A * x)) = [:(Seg (len A)),(Seg 1):] by A8, A11, A9, FINSEQ_1:def 3;
then A17: i in Seg (len A) by A14, ZFMISC_1:87;
then A18: i in dom (A * x) by A8, FINSEQ_1:def 3;
i in Seg (len ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x)))) by A7, A14, A16, ZFMISC_1:87;
then [i,j] in [:(Seg (len ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))))),(Seg (width ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))))):] by A15, ZFMISC_1:87;
then A19: [i,j] in Indices ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))) by FINSEQ_1:def 3;
j in Seg 1 by A9, A14, ZFMISC_1:87;
then ( 1 <= j & j <= 1 ) by FINSEQ_1:1;
then A20: j = 1 by XXREAL_0:1;
i in Seg (len (ColVec2Mx (A * x))) by A10, A14, A16, ZFMISC_1:87;
then [i,1] in Indices (ColVec2Mx (A * x)) by A13, ZFMISC_1:87;
then A21: ex p2 being FinSequence of REAL st
( p2 = (ColVec2Mx (A * x)) . i & (ColVec2Mx (A * x)) * (i,1) = p2 . 1 ) by MATRIX_0:def 5;
A22: (Col ((A * (ColVec2Mx x)),1)) . i = <*((A * x) . i)*> . 1
.= (ColVec2Mx (A * x)) * (i,1) by A3, A8, A18, A21, MATRIXR1:def 9 ;
len (A * (ColVec2Mx x)) = len A by A1, A4, MATRIX_3:def 4;
then i in dom (A * (ColVec2Mx x)) by A17, FINSEQ_1:def 3;
then (Col ((A * (ColVec2Mx x)),1)) . i = (A * (ColVec2Mx x)) * (i,j) by A20, MATRIX_0:def 8;
hence (MXR2MXF (ColVec2Mx (A * x))) * (i,j) = (Line ((MXR2MXF A),i)) "*" (Col ((MXR2MXF (ColVec2Mx x)),j)) by A5, A20, A22, A19, MATRIX_3:def 4; :: thesis: verum

end;

A23: len (MXR2MXF (ColVec2Mx (A * x))) = len (MXR2MXF A) by A3, A8, MATRIXR1:def 9;
width (MXR2MXF (ColVec2Mx (A * x))) = 1 by A3, A8, MATRIXR1:def 9
.= width (MXR2MXF (ColVec2Mx x)) by A2, MATRIXR1:def 9 ;
hence A * (ColVec2Mx x) = ColVec2Mx (A * x) by A23, A5, A12, MATRIX_3:def 4; :: thesis: verum