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

assume f is trivial ; :: thesis: len f is trivial

then dom f is trivial ;

hence len f is trivial by Lm1; :: thesis: verum