per cases ( a is zero or not a is zero ) ;

suppose a is zero ; :: thesis: a / (a * b) is light

hence a / (a * b) is light ; :: thesis: verum

end;

suppose not a is zero ; :: thesis: a / (a * b) is light

then (a * 1) / (a * b) = 1 / b by XCMPLX_1:91
.= b " ;
hence a / (a * b) is light ; :: thesis: verum

end;

end;