reconsider z9 = [*(opp x),(opp y)*] as Complex by Def2;
take z9 ; :: thesis: z + z9 = 0
A2: ( 0 = + (x,(opp x)) & 0 = + (y,(opp y)) ) by ARYTM_0:def 3;
0 in NAT ;
then reconsider zz = 0 as Element of REAL by NUMBERS:19;
0 = [*zz,zz*] by ARYTM_0:def 5;
hence z + z9 = 0 by A1, Def3, A2; :: thesis: verum