theorem :: FINSEQ_2:17

for a, b being object
for p, q being FinSequence st p ^ <*a*> = q ^ <*b*> holds
( p = q & a = b )