let a, b be Complex; :: 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 Lm19
.= (a + (- b)) * ((a * (- b)) ") by A1, Th211
.= (a + (- b)) * ((- (a * b)) ")
.= (a + (- b)) * (- ((a * b) ")) by Lm19
.= (b - a) * ((a * b) ") ; :: thesis: verum