let f be FinSequence; :: thesis: ( f is empty iff Rev f is empty )
thus ( f is empty implies Rev f is empty ) ; :: thesis: ( Rev f is empty implies f is empty )
assume Rev f is empty ; :: thesis: f is empty
then reconsider g = Rev f as empty FinSequence ;
Rev g is empty ;
hence f is empty ; :: thesis: verum