let a', b' be Element of REAL ; :: thesis: for a, b being real number st a' = a & b' = b holds
* a',b' = a * b
let a, b be real number ; :: thesis: ( a' = a & b' = b implies * a',b' = a * b )
assume A1: ( a' = a & b' = b ) ; :: thesis: * a',b' = a * b
consider x1, x2, y1, y2 being Element of REAL such that
A2: a = [*x1,x2*] and
A3: b = [*y1,y2*] and
A4: a * b = [*(+ (* x1,y1),(opp (* x2,y2))),(+ (* x1,y2),(* x2,y1))*] by XCMPLX_0:def 5;
A5: ( a = x1 & b = y1 ) by A2, A3, Lm2;
A6: ( x2 = 0 & y2 = 0 ) by A2, A3, Lm2;
then ( * x1,y2 = 0 & * x2,y1 = 0 ) by ARYTM_0:14;
then A7: + (* x1,y2),(* x2,y1) = 0 by ARYTM_0:13;
thus * a',b' = + (* x1,y1),(* (opp x2),y2) by A1, A5, A6, ARYTM_0:13, ARYTM_0:14
.= + (* x1,y1),(opp (* x2,y2)) by ARYTM_0:17
.= a * b by A4, A7, ARYTM_0:def 7 ; :: thesis: verum