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