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

per cases ( dom f is empty or ex x being object st dom f = {x} ) by A2, ZFMISC_1:131;

suppose dom f is empty ; :: thesis: len f is trivial

then f = {} ;
hence len f is trivial by CARD_1:27; :: thesis: verum

end;

suppose ex x being object st dom f = {x} ; :: thesis: len f is trivial

hence len f is trivial by A1, CARD_1:49, FINSEQ_3:20; :: thesis: verum

end;

end;