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