let c, a, b be complex number ; :: thesis: ( c <> 0 & a / c = b / c implies a = b )
assume A1: ( c <> 0 & a / c = b / c ) ; :: thesis: a = b
then a = (b / c) * c by Lm3;
hence a = b by A1, Lm3; :: thesis: verum