let D be non empty set ; :: thesis: for k, n, m being Nat
for e1, e2 being FinSequence of D st len e1 = m & len e2 = m holds
ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) )
let k, n, m be Nat; :: thesis: for e1, e2 being FinSequence of D st len e1 = m & len e2 = m holds
ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) )
let e1, e2 be FinSequence of D; :: thesis: ( len e1 = m & len e2 = m implies ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) ) )
assume A1: ( len e1 = m & len e2 = m ) ; :: thesis: ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) )
consider e being FinSequence of D * such that
A2: len e = n and
A3: for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) & ( not i in Seg k implies e . i = e2 ) ) by Th9;
A4: 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, A3; :: 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 A4; :: thesis: verum

end;

then e is Matrix of n,m,D by A2, MATRIX_0:def 2;
hence ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) ) by A3; :: thesis: verum