let D be non empty set ; :: thesis: for f being FinSequence of D st len f = 0 holds
Rev f = f
let f be FinSequence of D; :: thesis: ( len f = 0 implies Rev f = f )
assume len f = 0 ; :: thesis: Rev f = f
then A1: f = <*> D
.= {} ;
thus Rev f = f by A1; :: thesis: verum