let f be FinSequence; :: thesis: ( f is trivial implies len f is trivial )
assume f is trivial ; :: thesis: len f is trivial
then dom f is trivial ;
hence len f is trivial by Lm1; :: thesis: verum