let x be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st len A = len x holds
(LineVec2Mx x) * A = LineVec2Mx (x * A)
let A be Matrix of REAL; :: thesis: ( len A = len x implies (LineVec2Mx x) * A = LineVec2Mx (x * A) )
A1: len (LineVec2Mx (x * A)) = 1 by MATRIXR1:def 10;
assume A2: len A = len x ; :: thesis: (LineVec2Mx x) * A = LineVec2Mx (x * A)
then A3: width (MXR2MXF (LineVec2Mx x)) = len (MXR2MXF A) by MATRIXR1:def 10;
width (LineVec2Mx (x * A)) = len (x * A) by MATRIXR1:def 10;
then A4: width (LineVec2Mx (x * A)) = width A by A2, MATRIXR1:62;
A5: len (x * A) = width A by A2, MATRIXR1:62;
then A6: width (MXR2MXF (LineVec2Mx (x * A))) = width (MXR2MXF A) by MATRIXR1:def 10;
A7: width (LineVec2Mx x) = len x by MATRIXR1:def 10;
A8: for i, j being Nat st [i,j] in Indices (MXR2MXF (LineVec2Mx (x * A))) holds
(MXR2MXF (LineVec2Mx (x * A))) * (i,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j))

proof

len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)) = len (MXR2MXF (LineVec2Mx x)) by A3, MATRIX_3:def 4;
then len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)) = 1 by MATRIXR1:def 10;
then A9: 1 in Seg (len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A))) ;
let i, j be Nat; :: thesis: ( [i,j] in Indices (MXR2MXF (LineVec2Mx (x * A))) implies (MXR2MXF (LineVec2Mx (x * A))) * (i,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j)) )
A10: width ((LineVec2Mx x) * A) = width A by A2, A7, MATRIX_3:def 4;
assume A11: [i,j] in Indices (MXR2MXF (LineVec2Mx (x * A))) ; :: thesis: (MXR2MXF (LineVec2Mx (x * A))) * (i,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j))
then A12: j in Seg (width A) by A4, ZFMISC_1:87;
then j in dom (x * A) by A5, FINSEQ_1:def 3;
then A13: (Line (((LineVec2Mx x) * A),1)) . j = (LineVec2Mx (x * A)) * (1,j) by MATRIXR1:def 10;
Indices (LineVec2Mx (x * A)) = [:(Seg 1),(Seg (width A)):] by A1, A4, FINSEQ_1:def 3;
then i in Seg 1 by A11, ZFMISC_1:87;
then ( 1 <= i & i <= 1 ) by FINSEQ_1:1;
then A14: i = 1 by XXREAL_0:1;
width ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)) = width A by A3, MATRIX_3:def 4;
then [1,j] in [:(Seg (len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)))),(Seg (width ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)))):] by A12, A9, ZFMISC_1:87;
then A15: [1,j] in Indices ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)) by FINSEQ_1:def 3;
width (MXR2MXF (LineVec2Mx x)) = len (MXR2MXF A) by A2, MATRIXR1:def 10;
then ((LineVec2Mx x) * A) * (1,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j)) by A14, A15, MATRIX_3:def 4;
hence (MXR2MXF (LineVec2Mx (x * A))) * (i,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j)) by A12, A14, A13, A10, MATRIX_0:def 7; :: thesis: verum

end;

len (MXR2MXF (LineVec2Mx (x * A))) = len (MXR2MXF (LineVec2Mx x)) by A1, MATRIXR1:def 10;
hence (LineVec2Mx x) * A = LineVec2Mx (x * A) by A6, A3, A8, MATRIX_3:def 4; :: thesis: verum