let x9, y9 be Element of REAL ; for x, y being Real st x9 = x & y9 = y holds
+ (x9,y9) = x + y
let x, y be Real; ( x9 = x & y9 = y implies + (x9,y9) = x + y )
assume A1:
( x9 = x & y9 = y )
; + (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, Lm2;
then A4:
+ (x2,y2) = 0
by ARYTM_0:11;
( x = x1 & y = y1 )
by A2, Lm2;
hence
+ (x9,y9) = x + y
by A1, A3, A4, ARYTM_0:def 5; verum