theorem Lem8A: :: MSAFREE5:3

for p, q, r being FinSequence st p ^ q is_a_prefix_of p ^ r holds
q is_a_prefix_of r