let a, b, c be Complex; :: thesis: ( c <> 0 & a / c = b / c implies a = b )
assume that
A1: c <> 0 and
A2: a / c = b / c ; :: thesis: a = b
a = (b / c) * c by A1, A2, Lm3;
hence a = b by A1, Lm3; :: thesis: verum