let x, y be Element of REAL ; ( y = 1 implies * (x,y) = x )
assume A1:
y = 1
; * (x,y) = x
per cases
( x = 0 or x <> 0 )
;
suppose A2:
x <> 0
;
* (x,y) = xA5:
ex
x9,
y9 being
Element of
REAL+ st
(
y = x9 &
y = y9 &
* (
y,
y)
= x9 *' y9 )
by A1, Def2, ARYTM_2:20;
A6:
* (
x,
(inv x))
= 1
by A2, Def4;
* (
(* (x,y)),
(inv x)) =
* (
(* (x,(inv x))),
y)
by Th13
.=
* (
y,
y)
by A1, A2, Def4
.=
1
by A1, A5, ARYTM_2:15
;
hence
* (
x,
y)
= x
by A3, A6, Th18;
verum end; end;