let M be Matrix of REAL ; :: thesis: for p being FinSequence of REAL st len M = len p holds
for i being Element of NAT st i in Seg (len (p * M)) holds
(p * M) . i = p "*" (Col M,i)
let p be FinSequence of REAL ; :: thesis: ( len M = len p implies for i being Element of NAT st i in Seg (len (p * M)) holds
(p * M) . i = p "*" (Col M,i) )
assume A1: len M = len p ; :: thesis: for i being Element of NAT st i in Seg (len (p * M)) holds
(p * M) . i = p "*" (Col M,i)
A2: len (p * M) = len (Line ((LineVec2Mx p) * M),1) by MATRIXR1:def 12
.= width ((LineVec2Mx p) * M) by MATRIX_1:def 8 ;

hereby :: thesis: verum

let i be Element of NAT ; :: thesis: ( i in Seg (len (p * M)) implies p "*" (Col M,i) = (p * M) . i )
assume A3: i in Seg (len (p * M)) ; :: thesis: p "*" (Col M,i) = (p * M) . i
A4: width (LineVec2Mx p) = len M by A1, MATRIXR1:def 10;
then len ((LineVec2Mx p) * M) = len (LineVec2Mx p) by Th39;
then len ((LineVec2Mx p) * M) = 1 by MATRIXR1:48;
then 1 in Seg (len ((LineVec2Mx p) * M)) by FINSEQ_1:3;
then [1,i] in Indices ((LineVec2Mx p) * M) by A2, A3, Th12;
then A5: ((LineVec2Mx p) * M) * 1,i = (Line (LineVec2Mx p),1) "*" (Col M,i) by A4, Th39
.= p "*" (Col M,i) by MATRIXR1:48 ;
(Line ((LineVec2Mx p) * M),1) . i = ((LineVec2Mx p) * M) * 1,i by A2, A3, MATRIX_1:def 8;
hence p "*" (Col M,i) = (p * M) . i by A5, MATRIXR1:def 12; :: thesis: verum

end;