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) by Th71
.= (z1 + (- z2)) + z3 by FINSEQOP:28
.= (z1 - z2) + z3 ; :: thesis: verum