let x be FinSequence of REAL ; :: thesis: for M being Matrix of REAL st len x = width M & width M > 0 & x = (len x) |-> 1 holds
for k being Element of NAT st k in Seg (len (M * x)) holds
(M * x) . k = Sum (Line M,k)
let M be Matrix of REAL ; :: thesis: ( len x = width M & width M > 0 & x = (len x) |-> 1 implies for k being Element of NAT st k in Seg (len (M * x)) holds
(M * x) . k = Sum (Line M,k) )
assume A1: ( len x = width M & width M > 0 & x = (len x) |-> 1 ) ; :: thesis: for k being Element of NAT st k in Seg (len (M * x)) holds
(M * x) . k = Sum (Line M,k)

hereby :: thesis: verum

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

end;