let n, m be Nat; :: thesis: for D being non empty set
for F being Function of (Seg n),(Seg n)
for M being Matrix of n,m,D holds M * F is Matrix of n,m,D
let D be non empty set ; :: thesis: for F being Function of (Seg n),(Seg n)
for M being Matrix of n,m,D holds M * F is Matrix of n,m,D
let F be Function of (Seg n),(Seg n); :: thesis: for M being Matrix of n,m,D holds M * F is Matrix of n,m,D
let M be Matrix of n,m,D; :: thesis: M * F is Matrix of n,m,D
len M = n by MATRIX_1:def 3;
then ( dom F = Seg n & rng F c= Seg n & dom M = Seg n ) by FINSEQ_1:def 3, FUNCT_2:67, RELAT_1:def 19;
then A1: ( dom (M * F) = Seg n & n is Element of NAT ) by ORDINAL1:def 13, RELAT_1:46;
then reconsider Mp = M * F as FinSequence by FINSEQ_1:def 2;
A2: for x being set st x in rng Mp holds
ex p being FinSequence of D st
( x = p & len p = m )

proof

let x be set ; :: thesis: ( x in rng Mp implies ex p being FinSequence of D st
( x = p & len p = m ) )
assume A3: x in rng Mp ; :: thesis: ex p being FinSequence of D st
( x = p & len p = m )
( rng Mp c= rng M & rng M c= D * ) by FINSEQ_1:def 4, RELAT_1:45;
then x in D * by A3, TARSKI:def 3;
then reconsider p = x as FinSequence of D by FINSEQ_1:def 11;
take p ; :: thesis: ( x = p & len p = m )
p in rng M by A3, FUNCT_1:25;
hence ( x = p & len p = m ) by MATRIX_1:def 3; :: thesis: verum

end;

then reconsider Mp = Mp as Matrix of D by MATRIX_1:9;
( len Mp = n & ( for p being FinSequence of D st p in rng Mp holds
len p = m ) )

proof

thus len Mp = n by A1, FINSEQ_1:def 3; :: thesis: for p being FinSequence of D st p in rng Mp holds
len p = m
let p be FinSequence of D; :: thesis: ( p in rng Mp implies len p = m )
assume p in rng Mp ; :: thesis: len p = m
then ex q being FinSequence of D st
( p = q & len q = m ) by A2;
hence len p = m ; :: thesis: verum

end;

hence M * F is Matrix of n,m,D by MATRIX_1:def 3; :: thesis: verum