let x be FinSequence of REAL ; :: thesis: for M being Matrix of REAL st len x = len M & x = (len x) |-> 1 holds
for k being Element of NAT st k in Seg (len (x * M)) holds
(x * M) . k = Sum (Col M,k)
let M be Matrix of REAL ; :: thesis: ( len x = len M & x = (len x) |-> 1 implies for k being Element of 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 ; :: thesis: for k being Element of NAT st k in Seg (len (x * M)) holds
(x * M) . k = Sum (Col M,k)

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( k in Seg (len (x * M)) implies (x * M) . k = Sum (Col M,k) )
assume A3: k in Seg (len (x * M)) ; :: thesis: (x * M) . k = Sum (Col M,k)
A4: len (Col M,k) = len x by A1, MATRIX_1:def 9;
thus (x * M) . k = x "*" (Col M,k) by A1, A3, Th40
.= Sum (Col M,k) by A2, A4, Th32 ; :: thesis: verum

end;