let a, b be Complex; :: thesis: ( a * b = 1 implies a = 1 / b )
assume A1: a * b = 1 ; :: thesis: a = 1 / b
then b <> 0 ;
then a * 1 = 1 * (b ") by A1, XCMPLX_0:def 7;
hence a = 1 / b by Lm4; :: thesis: verum