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