let n, m be Nat; :: thesis: for D being non empty set
for M being Matrix of n,m,D
for F being Function of (Seg n),(Seg n)
for k being Nat st k in Seg n holds
Line ((M * F),k) = M . (F . k)
let D be non empty set ; :: thesis: for M being Matrix of n,m,D
for F being Function of (Seg n),(Seg n)
for k being Nat st k in Seg n holds
Line ((M * F),k) = M . (F . k)
let M be Matrix of n,m,D; :: thesis: for F being Function of (Seg n),(Seg n)
for k being Nat st k in Seg n holds
Line ((M * F),k) = M . (F . k)
let F be Function of (Seg n),(Seg n); :: thesis: for k being Nat st k in Seg n holds
Line ((M * F),k) = M . (F . k)
let k be Nat; :: thesis: ( k in Seg n implies Line ((M * F),k) = M . (F . k) )
assume A1: k in Seg n ; :: thesis: Line ((M * F),k) = M . (F . k)
len (M * F) = n by MATRIX_0:def 2;
then k in dom (M * F) by A1, FINSEQ_1:def 3;
then (M * F) . k = M . (F . k) by FUNCT_1:12;
hence Line ((M * F),k) = M . (F . k) by A1, MATRIX_0:52; :: thesis: verum