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