let a, b be Complex; :: thesis: ( a / b = 1 implies a = b )
assume A1: a / b = 1 ; :: thesis: a = b
then b <> 0 by Th49;
then a = 1 * b by A1, Lm3;
hence a = b ; :: thesis: verum