per cases ( x in dom p or not x in dom p ) ;

suppose x in dom p ; :: thesis: ( p . x is finite & p . x is Function-like & p . x is Relation-like )

hence ( p . x is finite & p . x is Function-like & p . x is Relation-like ) by Def1; :: thesis: verum

end;

suppose not x in dom p ; :: thesis: ( p . x is finite & p . x is Function-like & p . x is Relation-like )

hence ( p . x is finite & p . x is Function-like & p . x is Relation-like ) by FUNCT_1:def 2; :: thesis: verum

end;

end;