let D be non empty set ; :: thesis: for m, n being Nat
for e1 being FinSequence of D st len e1 = m holds
n |-> e1 is Matrix of n,m,D
let m, n 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 FINSEQ_1:def 18;
A3: for i being Element of NAT st i in dom e holds
len (e . i) = m

proof

let i be Element of 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:13; :: 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 set st
( i in dom e & p = e . i ) by FUNCT_1:def 5;
hence len p = m by A3; :: thesis: verum

end;

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