theorem Th2: :: PRGCOR_2:2

for D being non empty set
for q being FinSequence of D
for n being Nat st NAT c= D & n > len q holds
ex p being XFinSequence of D st
( len p = n & p is_an_xrep_of q )