theorem :: BINARI_3:3
for t1, t2 being FinSequence st Rev t1 = Rev t2 holds
t1 = t2