let f be FinSequence; :: thesis: ( dom f is trivial implies len f is trivial )
assume A1: dom f is trivial ; :: thesis: len f is trivial
A2: Seg (len f) = dom f by FINSEQ_1:def 3;

per cases ( dom f is empty or ex x being set st dom f = {x} ) by A1, REALSET1:def 4;

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

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

end;

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

hence len f is trivial by A2, CARD_1:87, FINSEQ_3:22; :: thesis: verum

end;

end;