let m, n be Nat; :: thesis: for D being non empty set
for a being Element of D holds m |-> (n |-> a) is Matrix of m,n,D
let D be non empty set ; :: thesis: for a being Element of D holds m |-> (n |-> a) is Matrix of m,n,D
let a be Element of D; :: thesis: m |-> (n |-> a) is Matrix of m,n,D
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 13;
reconsider d = n1 |-> a as Element of D * by FINSEQ_1:def 11;
reconsider M = m1 |-> d as FinSequence of D * ;
reconsider M = M as Matrix of D by Th2;
M is Matrix of m,n,D

proof

thus len M = m by FINSEQ_1:def 18; :: according to MATRIX_1:def 3 :: thesis: for p being FinSequence of D st p in rng M holds
len p = n
let p be FinSequence of D; :: thesis: ( p in rng M implies len p = n )
A1: rng M c= {(n |-> a)} by FUNCOP_1:19;
assume p in rng M ; :: thesis: len p = n
then p = n |-> a by A1, TARSKI:def 1;
hence len p = n by FINSEQ_1:def 18; :: thesis: verum

end;

hence m |-> (n |-> a) is Matrix of m,n,D ; :: thesis: verum