let a, b be Complex; :: thesis: ( 1 / a = 1 / b implies a = b )
assume 1 / a = 1 / b ; :: thesis: a = b
then a " = 1 / b by Lm4;
then a " = b " by Lm4;
hence a = b by Lm12; :: thesis: verum