theorem Th5: :: REWRITE2:5

for s being XFinSequence
for p being XFinSequence-yielding FinSequence holds
( len (s ^+ p) = len p & len (p +^ s) = len p )