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