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