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

end;

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;