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