let x9, y9 be Element of REAL ; :: thesis: for x, y being real number st x9 = x & y9 = y holds
* x9,y9 = x * y
let x, y be real number ; :: thesis: ( x9 = x & y9 = y implies * x9,y9 = x * y )
assume A1: ( x9 = x & y9 = y ) ; :: thesis: * 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:14;
A6: y2 = 0 by A3, Lm7;
then * x1,y2 = 0 by ARYTM_0:14;
then A7: + (* x1,y2),(* x2,y1) = 0 by A5, ARYTM_0:13;
( x = x1 & y = y1 ) by A2, A3, Lm7;
hence * x9,y9 = + (* x1,y1),(* (opp x2),y2) by A1, A6, ARYTM_0:13, ARYTM_0:14
.= + (* x1,y1),(opp (* x2,y2)) by ARYTM_0:17
.= x * y by A4, A7, ARYTM_0:def 7 ;
:: thesis: verum