let n be Element of NAT ; :: thesis: for z1, z2, z3 being Element of COMPLEX n holds z1 + (z2 - z3) = (z1 + z2) - z3
let z1, z2, z3 be Element of COMPLEX n; :: thesis: z1 + (z2 - z3) = (z1 + z2) - z3
thus z1 + (z2 - z3) = z1 + (z2 + (- z3))
.= (z1 + z2) + (- z3) by FINSEQOP:29
.= (z1 + z2) - z3 ; :: thesis: verum