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;