let f be FinSequence of R; :: thesis: ( f is empty implies f is trivial )
assume f is empty ; :: thesis: f is trivial
then f = <*> the carrier of R ;
hence f is trivial ; :: thesis: verum