let M be Matrix of REAL; for p being FinSequence of REAL st width M = len p & width M > 0 holds
for i being Nat st i in Seg (len (M * p)) holds
(M * p) . i = (Line (M,i)) "*" p
let p be FinSequence of REAL ; ( width M = len p & width M > 0 implies for i being Nat st i in Seg (len (M * p)) holds
(M * p) . i = (Line (M,i)) "*" p )
assume A1:
( width M = len p & width M > 0 )
; for i being Nat st i in Seg (len (M * p)) holds
(M * p) . i = (Line (M,i)) "*" p
A2: len (M * p) =
len (Col ((M * (ColVec2Mx p)),1))
by MATRIXR1:def 11
.=
len (M * (ColVec2Mx p))
by MATRIX_0:def 8
;
hereby verum
let i be
Nat;
( i in Seg (len (M * p)) implies (Line (M,i)) "*" p = (M * p) . i )assume A3:
i in Seg (len (M * p))
;
(Line (M,i)) "*" p = (M * p) . i
i in dom (M * (ColVec2Mx p))
by A2, A3, FINSEQ_1:def 3;
then A4:
(Col ((M * (ColVec2Mx p)),1)) . i = (M * (ColVec2Mx p)) * (
i,1)
by MATRIX_0:def 8;
A5:
len (ColVec2Mx p) = width M
by A1, MATRIXR1:def 9;
then
width (M * (ColVec2Mx p)) = width (ColVec2Mx p)
by Th39;
then
width (M * (ColVec2Mx p)) = 1
by A1, MATRIXR1:def 9;
then
1
in Seg (width (M * (ColVec2Mx p)))
;
then
[i,1] in Indices (M * (ColVec2Mx p))
by A2, A3, Th12;
then (M * (ColVec2Mx p)) * (
i,1) =
(Line (M,i)) "*" (Col ((ColVec2Mx p),1))
by A5, Th39
.=
(Line (M,i)) "*" p
by A1, MATRIXR1:45
;
hence
(Line (M,i)) "*" p = (M * p) . i
by A4, MATRIXR1:def 11;
verum
end;