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: (Line ((LineVec2Mx p) * M),1) . i = ((LineVec2Mx p) * M) * 1,i by A2, A3, MATRIX_1:def 8;
A5: width (LineVec2Mx p) = len M by A1, MATRIXR1:def 10;
then ( len ((LineVec2Mx p) * M) = len (LineVec2Mx p) & width ((LineVec2Mx p) * M) = width M ) by Th39;
then ( len ((LineVec2Mx p) * M) = 1 & width ((LineVec2Mx p) * M) = width M ) by MATRIXR1:48;
then ( 1 in Seg (len ((LineVec2Mx p) * M)) & i in Seg (width ((LineVec2Mx p) * M)) ) by A2, A3, FINSEQ_1:3;
then [1,i] in Indices ((LineVec2Mx p) * M) by Th12;
then ((LineVec2Mx p) * M) * 1,i = (Line (LineVec2Mx p),1) "*" (Col M,i) by A5, Th39
.= p "*" (Col M,i) by MATRIXR1:48 ;
hence p "*" (Col M,i) = (p * M) . i by A4, MATRIXR1:def 12; :: thesis: verum

end;