let t1, t2 be FinSequence; :: thesis: ( Rev t1 = Rev t2 implies t1 = t2 )

assume A1: Rev t1 = Rev t2 ; :: thesis: t1 = t2

thus t1 = Rev (Rev t1)

.= t2 by A1 ; :: thesis: verum

assume A1: Rev t1 = Rev t2 ; :: thesis: t1 = t2

thus t1 = Rev (Rev t1)

.= t2 by A1 ; :: thesis: verum