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_1:def 3;
then k in dom (M * F) by A1, FINSEQ_1:def 3;
then (M * F) . k = M . (F . k) by FUNCT_1:22;
hence Line (M * F),k = M . (F . k) by A1, MATRIX_2:10; :: thesis: verum