let x9, y9 be Element of REAL ; for x, y being Real st x9 = x & y9 = y holds
* (x9,y9) = x * y
let x, y be Real; ( x9 = x & y9 = y implies * (x9,y9) = x * y )
assume A1:
( x9 = x & y9 = y )
; * (x9,y9) = x * y
consider x1, x2, y1, y2 being Element of REAL such that
A2:
x = [*x1,x2*]
and
A3:
y = [*y1,y2*]
and
A4:
x * y = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*]
by XCMPLX_0:def 5;
x2 = 0
by A2, Lm7;
then A5:
* (x2,y1) = 0
by ARYTM_0:12;
A6:
y2 = 0
by A3, Lm7;
then
* (x1,y2) = 0
by ARYTM_0:12;
then A7:
+ ((* (x1,y2)),(* (x2,y1))) = 0
by A5, ARYTM_0:11;
( x = x1 & y = y1 )
by A2, A3, Lm7;
hence * (x9,y9) =
+ ((* (x1,y1)),(* ((opp x2),y2)))
by A1, A6, ARYTM_0:11, ARYTM_0:12
.=
+ ((* (x1,y1)),(opp (* (x2,y2))))
by ARYTM_0:15
.=
x * y
by A4, A7, ARYTM_0:def 5
;
verum