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