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