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

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