let n, m be Nat; 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 ; for a being Element of D holds m |-> (n |-> a) is Matrix of m,n,D
let a be Element of D; m |-> (n |-> a) is Matrix of m,n,D
reconsider n1 = n, m1 = m as Nat ;
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 m,n -size
hence
m |-> (n |-> a) is Matrix of m,n,D
; verum