let n, m 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 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

proof

thus len M = m by CARD_1:def 7; :: according to MATRIX_0:def 2 :: 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:13;
assume p in rng M ; :: thesis: len p = n
then p = n |-> a by A1, TARSKI:def 1;
hence len p = n by CARD_1:def 7; :: thesis: verum

end;

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