set p = (Seg n) --> {} ;
A1: 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 FUNCOP_1:19, Th8; :: according to FINSEQ_1:def 18 :: thesis: verum