let a, b be Complex; :: thesis: (a / b) " = b / a

per cases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;

suppose A1: a = 0 ; :: thesis: (a / b) " = b / a

hence (a / b) " = b * (0 ")
.= b / a by A1, XCMPLX_0:def 9 ;
:: thesis: verum

end;

suppose A2: b = 0 ; :: thesis: (a / b) " = b / a

hence (a / b) " = (a * (0 ")) " by XCMPLX_0:def 9
.= b / a by A2 ;
:: thesis: verum

end;

suppose A3: ( a <> 0 & b <> 0 ) ; :: thesis: (a / b) " = b / a

(a / b) * (b / a) = (a * b) / (a * b) by Lm6;
then (a / b) * (b / a) = 1 by A3, Lm5;
hence (a / b) " = b / a by A3, XCMPLX_0:def 7; :: thesis: verum

end;

end;