set p = (Seg n) --> {};
dom ((Seg n) --> {}) = Seg n by FUNCOP_1:13;
then reconsider p = (Seg n) --> {} as FinSequence by Def2;
take p ; :: thesis: p is n -element
Seg (len p) = dom p by Def3;
hence len p = n by Th8, FUNCOP_1:13; :: according to CARD_1:def 7 :: thesis: verum