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