theorem Th82: :: MSAFREE4:82

for x, y being set
for p, q being FinSequence holds ((p ^ <*x*>) ^ q) +* (((len p) + 1),y) = (p ^ <*y*>) ^ q