let b, a be complex number ; :: 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, Th107 ; :: thesis: verum