let a, b be Integer; :: thesis: for c being Nat holds [\(a / (b * c))/] = [\([\(a / b)/] / c)/]
let c be Nat; :: thesis: [\(a / (b * c))/] = [\([\(a / b)/] / c)/]

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

suppose ( b = 0 or c = 0 ) ; :: thesis: [\(a / (b * c))/] = [\([\(a / b)/] / c)/]

then ( a / (b * c) = 0 & ( a / b = 0 or [\(a / b)/] / c = 0 ) ) ;
hence [\(a / (b * c))/] = [\([\(a / b)/] / c)/] ; :: thesis: verum

end;

suppose B1: ( b <> 0 & c <> 0 ) ; :: thesis: [\(a / (b * c))/] = [\([\(a / b)/] / c)/]

then reconsider b = b as non zero Integer ;
reconsider c = c as positive Integer by B1;
[\(a / (b * c))/] = [\((a / b) / c)/] by XCMPLX_1:78
.= [\([\(a / b)/] / c)/] by FFP ;
hence [\(a / (b * c))/] = [\([\(a / b)/] / c)/] ; :: thesis: verum

end;

end;