let M be Matrix of REAL; 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 ; ( 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
; 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 verum
let i be
Nat;
( i in Seg (len (p * M)) implies p "*" (Col (M,i)) = (p * M) . i )assume A3:
i in Seg (len (p * M))
;
p "*" (Col (M,i)) = (p * M) . iA4:
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;
verum
end;