per
cases
( (
a
in
[.
0
,1
.]
&
b
in
[.
0
,1
.]
) or not
a
in
[.
0
,1
.]
or not
b
in
[.
0
,1
.]
)
;
suppose
(
a
in
[.
0
,1
.]
&
b
in
[.
0
,1
.]
) ;
:: thesis:
f
.
(
a
,
b
) is
real
then
f
.
(
a
,
b
)
in
[.
0
,1
.]
by
BINOP_1:17
;
hence
f
.
(
a
,
b
) is
real
;
:: thesis:
verum
end;
suppose
( not
a
in
[.
0
,1
.]
or not
b
in
[.
0
,1
.]
) ;
:: thesis:
f
.
(
a
,
b
) is
real
then
not
[
a
,
b
]
in
dom
f
by
ZFMISC_1:87
;
hence
f
.
(
a
,
b
) is
real
by
FUNCT_1:def 2
;
:: thesis:
verum
end;
end;