let M be Matrix of REAL; :: thesis: for p being FinSequence of REAL st len M = len p holds
for i being 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 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 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_0:def 7 ;

hereby :: thesis: verum

let i be 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)) ;
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_0:def 7;
hence p "*" (Col (M,i)) = (p * M) . i by A5, MATRIXR1:def 12; :: thesis: verum

end;