let z1, z2 be Element of COMPLEX ; :: thesis: (z1 - z2) *' = (z1 *' ) - (z2 *' )
thus (z1 - z2) *' = (z1 + (- z2)) *'
.= (z1 *' ) + ((- z2) *' ) by Th118
.= (z1 *' ) + (- (z2 *' )) by Th119
.= (z1 *' ) - (z2 *' ) ; :: thesis: verum