let z1, z2 be Complex; :: thesis: (z1 - z2) *' = (z1 *') - (z2 *')
thus (z1 - z2) *' = (z1 + (- z2)) *'
.= (z1 *') + ((- z2) *') by Th32
.= (z1 *') + (- (z2 *')) by Th33
.= (z1 *') - (z2 *') ; :: thesis: verum