theorem Th7: :: FINSEQ_6:7

for f1, f2 being FinSequence
for p being set st p in (rng f2) \ (rng f1) holds
p .. (f1 ^ f2) = (len f1) + (p .. f2)