for D being non empty set
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 ) )