let x be FinSequence of REAL ; for M being Matrix of REAL st len x = len M & x = (len x) |-> 1 holds
for k being Nat st k in Seg (len (x * M)) holds
(x * M) . k = Sum (Col (M,k))
let M be Matrix of REAL; ( len x = len M & x = (len x) |-> 1 implies for k being Nat st k in Seg (len (x * M)) holds
(x * M) . k = Sum (Col (M,k)) )
assume that
A1:
len x = len M
and
A2:
x = (len x) |-> 1
; for k being Nat st k in Seg (len (x * M)) holds
(x * M) . k = Sum (Col (M,k))
hereby verum
let k be
Nat;
( k in Seg (len (x * M)) implies (x * M) . k = Sum (Col (M,k)) )assume A3:
k in Seg (len (x * M))
;
(x * M) . k = Sum (Col (M,k))A4:
len (Col (M,k)) = len x
by A1, MATRIX_0:def 8;
thus (x * M) . k =
x "*" (Col (M,k))
by A1, A3, Th40
.=
Sum (Col (M,k))
by A2, A4, Th32
;
verum
end;