let D be non empty set ; :: thesis: for k being Element of NAT
for m, n 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 be Element of NAT ; :: thesis: for m, n 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 m, n 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 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, 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 set st
( i in dom e & p = e . i ) by FUNCT_1:def 5;
hence len p = m by A4; :: thesis: verum

end;

then e is Matrix of n,m,D by A2, MATRIX_1:def 3;
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