let x, y, z be Complex; :: thesis: ( z = x + y implies Re z = (Re x) + (Re y) )
assume A1: z = x + y ; :: thesis: Re z = (Re x) + (Re 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;
A4: ( Re x = x1 & Re y = y1 ) by A2, Lm2;
thus Re z = + (x1,y1) by A1, A3, Lm2
.= (Re x) + (Re y) by A4, Lm8 ; :: thesis: verum