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