theorem Th2: :: MATRPROB:2

for D being non empty set
for k, n being Nat
for a, b being Element of D ex g being FinSequence of D st
( len g = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies g . i = a ) & ( not i in Seg k implies g . i = b ) ) ) )