per
cases
(
j
in
dom
B
or not
j
in
dom
B
)
;
suppose
j
in
dom
B
;
:: thesis:
(
B
.
j
is
Function-like
&
B
.
j
is
Relation-like
)
hence
(
B
.
j
is
Function-like
&
B
.
j
is
Relation-like
)
by
Def6
;
:: thesis:
verum
end;
suppose
not
j
in
dom
B
;
:: thesis:
(
B
.
j
is
Function-like
&
B
.
j
is
Relation-like
)
hence
(
B
.
j
is
Function-like
&
B
.
j
is
Relation-like
)
by
FUNCT_1:def 2
;
:: thesis:
verum
end;
end;