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