theorem Th2: :: REWRITE1:2

for p, q being FinSequence
for x being object st q <> {} holds
(p ^ <*x*>) $^ q = p ^ q