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