theorem :: REWRITE1:3

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