let n be 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:28
.= z1 - (z2 + z3) by Th65 ; :: thesis: verum