theorem :: AFINSQ_1:62

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