let z, z1 be Element of F_Complex; :: thesis: z1 = (z1 + z) - z
reconsider z19 = z1, z9 = z as Element of COMPLEX by Def1;
thus (z1 + z) - z = (z19 + z9) - z9 by Th3
.= z1 ; :: thesis: verum