let z1, z2 be Element of F_Complex ; (z1 - z2) *' = (z1 *' ) - (z2 *' )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
z19 - z29 = z1 - z2
by Th5;
hence (z1 - z2) *' =
(z19 *' ) - (z29 *' )
by COMPLEX1:120
.=
(z1 *' ) - (z2 *' )
by Th5
;
verum