theorem Th15: :: POLYFORM:17

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