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 f = <*> D
.= {} ;
hence Rev f = f ; :: thesis: verum