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