let x9, y9 be Element of REAL ; :: thesis: for x, y being Real st x9 = x & y9 = y holds
+ (x9,y9) = x + y
let x, y be Real; :: thesis: ( x9 = x & y9 = y implies + (x9,y9) = x + y )
assume A1: ( x9 = x & y9 = y ) ; :: thesis: + (x9,y9) = x + y
consider x1, x2, y1, y2 being Element of REAL such that
A2: ( x = [*x1,x2*] & y = [*y1,y2*] ) and
A3: x + y = [*(+ (x1,y1)),(+ (x2,y2))*] by XCMPLX_0:def 4;
( x2 = 0 & y2 = 0 ) by A2, Lm7;
then A4: + (x2,y2) = 0 by ARYTM_0:11;
( x = x1 & y = y1 ) by A2, Lm7;
hence + (x9,y9) = x + y by A1, A3, A4, ARYTM_0:def 5; :: thesis: verum