theorem Lem9: :: BAGORD_2:8

for a being object
for p being FinSequence st a in rng p holds
ex q, r being FinSequence st p = (q ^ <*a*>) ^ r