consider n being Nat such that
A1: dom p = Seg n by Def2;
dom (disjoin p) = dom p by CARD_3:def 3;
hence disjoin p is FinSequence-like by A1; :: thesis: verum