let a be Real; :: thesis: for b being negative Integer holds [\(a / b)/] = [\([/a\] / b)/]
let b be negative Integer; :: thesis: [\(a / b)/] = [\([/a\] / b)/]
reconsider k = - b as positive Integer ;
[\(a / b)/] = [\(a / (- k))/]
.= [\((- a) / k)/] by XCMPLX_1:192
.= [\([\(- a)/] / k)/] by FFP
.= [\((- [\(- a)/]) / b)/] by XCMPLX_1:192 ;
hence [\(a / b)/] = [\([/a\] / b)/] by FCB; :: thesis: verum