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