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