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