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