theorem :: FINSEQ_2:143

for x being object
for m, n being Nat st n |-> x = m |-> x holds
n = m