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),(+ x2,y2)*] by XCMPLX_0:def 4;
A5: ( a = x1 & b = y1 ) by A2, A3, Lm2;
( x2 = 0 & y2 = 0 ) by A2, A3, Lm2;
then + x2,y2 = 0 by ARYTM_0:13;
hence + a',b' = a + b by A1, A4, A5, ARYTM_0:def 7; :: thesis: verum