reconsider z9 = [*(opp x),(opp y)*] as complex number by Def2;
take z9 ; :: thesis: z + z9 = 0
A3: ( 0 = + x,(opp x) & 0 = + y,(opp y) ) by ARYTM_0:def 4;
thus z + z9 = 0 by A2, A3, Def4, Lm1; :: thesis: verum