dom (F * p) = dom p by PARTFUN1:def 2;
hence ex n being Nat st dom (F * p) = Seg n by FINSEQ_1:def 2; :: according to FINSEQ_1:def 2 :: thesis: verum