1 in dom p by FINSEQ_5:6;
hence ( p . 1 is Function-like & p . 1 is Relation-like ) ; :: thesis: verum