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)),(+ (x2,y2))*] by XCMPLX_0:def 4;
A6: y2 = 0 by A4, Lm2;
x2 = 0 by A3, Lm2;
then A7: + (x2,y2) = 0 by A6, ARYTM_0:11;
A8: b = y1 by A4, Lm2;
a = x1 by A3, Lm2;
hence + (a9,b9) = a + b by A1, A2, A5, A8, A7, ARYTM_0:def 5; :: thesis: verum