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