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
A1: rng F c= Seg n by RELAT_1:def 19;
len M = n by MATRIX_0:def 2;
then A2: dom M = Seg n by FINSEQ_1:def 3;
dom F = Seg n by FUNCT_2:52;
then A3: dom (M * F) = Seg n by A1, A2, RELAT_1:27;
then reconsider Mp = M * F as FinSequence by FINSEQ_1:def 2;
A4: for x being object st x in rng Mp holds
ex p being FinSequence of D st
( x = p & len p = m )

proof

A5: rng M c= D * by FINSEQ_1:def 4;
let x be object ; :: thesis: ( x in rng Mp implies ex p being FinSequence of D st
( x = p & len p = m ) )
assume A6: x in rng Mp ; :: thesis: ex p being FinSequence of D st
( x = p & len p = m )
rng Mp c= rng M by RELAT_1:26;
then x in D * by A6, A5;
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 A6, FUNCT_1:14;
hence ( x = p & len p = m ) by MATRIX_0:def 2; :: thesis: verum

end;

then reconsider Mp = Mp as Matrix of D by MATRIX_0:9;
A7: n is Element of NAT by ORDINAL1:def 12;
( len Mp = n & ( for p being FinSequence of D st p in rng Mp holds
len p = m ) )

proof

thus len Mp = n by A3, A7, 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 A4;
hence len p = m ; :: thesis: verum

end;

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