let z1, z2 be Element of F_Complex; :: thesis: z1 - (- z2) = z1 + z2
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
- z2 = - z29 by Th2;
hence z1 - (- z2) = z19 - (- z29) by Th3
.= z1 + z2 ;
:: thesis: verum