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