let f be FinSequence; :: thesis: ( dom f is trivial implies len f is trivial )

A1: Seg (len f) = dom f by FINSEQ_1:def 3;

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

A1: Seg (len f) = dom f by FINSEQ_1:def 3;

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