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