let D be non empty set ; :: thesis: for n, m being Nat
for e1 being FinSequence of D st len e1 = m holds
n |-> e1 is Matrix of n,m,D
let n, m be Nat; :: thesis: for e1 being FinSequence of D st len e1 = m holds
n |-> e1 is Matrix of n,m,D
let e1 be FinSequence of D; :: thesis: ( len e1 = m implies n |-> e1 is Matrix of n,m,D )
assume A1: len e1 = m ; :: thesis: n |-> e1 is Matrix of n,m,D
reconsider e = n |-> e1 as FinSequence of D * by Th8;
A2: len e = n by CARD_1:def 7;
A3: for i being Nat st i in dom e holds
len (e . i) = m

proof

let i be Nat; :: thesis: ( i in dom e implies len (e . i) = m )
assume i in dom e ; :: thesis: len (e . i) = m
then i in Seg n by A2, FINSEQ_1:def 3;
hence len (e . i) = m by A1, FUNCOP_1:7; :: thesis: verum

end;

then reconsider e = e as Matrix of D by Th11;
for p being FinSequence of D st p in rng e holds
len p = m

proof

let p be FinSequence of D; :: thesis: ( p in rng e implies len p = m )
assume p in rng e ; :: thesis: len p = m
then ex i being object st
( i in dom e & p = e . i ) by FUNCT_1:def 3;
hence len p = m by A3; :: thesis: verum

end;

hence n |-> e1 is Matrix of n,m,D by A2, MATRIX_0:def 2; :: thesis: verum