theorem Th7: :: GRAPH_5:9

for p, q being FinSequence
for x being object st q ^ <*x*> is one-to-one & rng (q ^ <*x*>) c= rng p holds
ex p1, p2 being FinSequence st
( p = (p1 ^ <*x*>) ^ p2 & rng q c= rng (p1 ^ p2) )