theorem Th2: :: REWRITE2:2

for k being Nat
for p, q being FinSequence st k > len p & k <= len (p ^ q) holds
ex l being Nat st
( k = (len p) + l & l >= 1 & l <= len q )