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 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 Nat st k in Seg (len (M * x)) holds
(M * x) . k = Sum (Line (M,k)) )
assume that
A1: len x = width M and
A2: width M > 0 and
A3: x = (len x) |-> 1 ; :: thesis: for k being Nat st k in Seg (len (M * x)) holds
(M * x) . k = Sum (Line (M,k))

hereby :: thesis: verum

let k be Nat; :: thesis: ( k in Seg (len (M * x)) implies (M * x) . k = Sum (Line (M,k)) )
assume A4: k in Seg (len (M * x)) ; :: thesis: (M * x) . k = Sum (Line (M,k))
A5: len (Line (M,k)) = len x by A1, MATRIX_0:def 7;
thus (M * x) . k = (Line (M,k)) "*" x by A1, A2, A4, Th41
.= Sum (Line (M,k)) by A3, A5, Th32 ; :: thesis: verum

end;