per
cases
(
A
<>
{}
or
A
=
{}
)
;
suppose
A
<>
{}
;
:: thesis:
f
.
(
a
,
b
) is
Element
of
A
then
reconsider
A
=
A
as non
empty
set
;
reconsider
f
=
f
as
BinOp
of
A
;
reconsider
ab
=
[
a
,
b
]
as
Element
of
[:
A
,
A
:]
by
ZFMISC_1:def 2
;
f
.
ab
is
Element
of
A
;
hence
f
.
(
a
,
b
) is
Element
of
A
;
:: thesis:
verum
end;
suppose
A1
:
A
=
{}
;
:: thesis:
f
.
(
a
,
b
) is
Element
of
A
then
not
[
a
,
b
]
in
dom
f
;
then
f
.
(
a
,
b
)
=
{}
by
FUNCT_1:def 2
;
hence
f
.
(
a
,
b
) is
Element
of
A
by
A1
,
SUBSET_1:def 1
;
:: thesis:
verum
end;
end;