theorem :: REWRITE1:4

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