theorem Th6: :: FSM_3:6

for x, y being set
for p, q being XFinSequence st <%x%> ^ p = <%y%> ^ q holds
( x = y & p = q )