let a, b, c be complex number ; :: thesis: (a / b) * c = ((1 / b) * c) * a
(a / b) * c = ((1 / b) * a) * c by Lm15;
hence (a / b) * c = ((1 / b) * c) * a ; :: thesis: verum