let
x
,
y
be
ExtReal
;
:: thesis:
(
0
<=
x
*
y
implies
.
(
x
+
y
)
.
=
.
x
.
+
.
y
.
)
assume
A1
:
0
<=
x
*
y
;
:: thesis:
.
(
x
+
y
)
.
=
.
x
.
+
.
y
.
per
cases
( ( (
0
<=
x
or
0
<
x
) & (
0
<=
y
or
0
<
y
) ) or ( (
x
<=
0
or
x
<
0
) & (
y
<=
0
or
y
<
0
) ) )
by
A1
;
suppose
( (
0
<=
x
or
0
<
x
) & (
0
<=
y
or
0
<
y
) ) ;
:: thesis:
.
(
x
+
y
)
.
=
.
x
.
+
.
y
.
then
(
.
x
.
=
x
&
.
y
.
=
y
)
by
Def1
;
hence
.
(
x
+
y
)
.
=
.
x
.
+
.
y
.
by
Def1
;
:: thesis:
verum
end;
suppose
A2
: ( (
x
<=
0
or
x
<
0
) & (
y
<=
0
or
y
<
0
) ) ;
:: thesis:
.
(
x
+
y
)
.
=
.
x
.
+
.
y
.
then
A3
:
.
(
x
+
y
)
.
=

(
x
+
y
)
by
Th7
.=
(

x
)

y
by
XXREAL_3:25
;
.
x
.
=

x
by
A2
,
Th7
;
hence
.
(
x
+
y
)
.
=
.
x
.
+
.
y
.
by
A2
,
A3
,
Th7
;
:: thesis:
verum
end;
end;