let a, b be complex number ; :: thesis: ( a <> 0 & b <> 0 implies (a " ) - (b " ) = (b - a) * ((a * b) " ) )
assume A1: ( a <> 0 & b <> 0 ) ; :: thesis: (a " ) - (b " ) = (b - a) * ((a * b) " )
thus (a " ) - (b " ) = (a " ) + (- (b " ))
.= (a " ) + ((- b) " ) by Lm20
.= (a + (- b)) * ((a * (- b)) " ) by A1, Th213
.= (a + (- b)) * ((- (a * b)) " )
.= (a + (- b)) * (- ((a * b) " )) by Lm20
.= (b - a) * ((a * b) " ) ; :: thesis: verum