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 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 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 Nat st k in Seg (len (x * M)) holds
(x * M) . k = Sum (Col (M,k))

hereby :: thesis: verum

let k be 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_0:def 8;
thus (x * M) . k = x "*" (Col (M,k)) by A1, A3, Th40
.= Sum (Col (M,k)) by A2, A4, Th32 ; :: thesis: verum

end;