theorem :: FINSEQ_1:76

for a, b being object st <*a*> = <*b*> holds
a = b