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 A1: ( len x = len M & 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 A2: k in Seg (len (x * M)) ; :: thesis: (x * M) . k = Sum (Col M,k)
A3: len (Col M,k) = len x by A1, MATRIX_1:def 9;
thus (x * M) . k = x "*" (Col M,k) by A1, A2, Th40
.= Sum (Col M,k) by A1, A3, Th32 ; :: thesis: verum

end;