let z1, z2 be Element of F_Complex ; :: thesis: z1 - (- z2) = z1 + z2
reconsider z1' = z1, z2' = z2 as Element of COMPLEX by Def1;
- z2 = - z2' by Th4;
hence z1 - (- z2) = z1' - (- z2') by Th5
.= z1 + z2 ;
:: thesis: verum