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

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