let a, b, c be Complex; :: thesis: ( a <> 0 implies (a * b) + c = a * (b + (c / a)) )
assume a <> 0 ; :: thesis: (a * b) + c = a * (b + (c / a))
hence (a * b) + c = (a * b) + (a * (c / a)) by Lm3
.= a * (b + (c / a)) ;
:: thesis: verum