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