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