let a, b, c be Complex; :: thesis: (a / b) * c = ((1 / b) * c) * a
(a / b) * c = ((1 / b) * a) * c by Lm14;
hence (a / b) * c = ((1 / b) * c) * a ; :: thesis: verum