let a, b be Real; :: thesis: [\(a / b)/] = [\([\a/] / b)/] + [\((frac ([\a/] / b)) + ((frac a) / b))/]

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

suppose b = 0 ; :: thesis: [\(a / b)/] = [\([\a/] / b)/] + [\((frac ([\a/] / b)) + ((frac a) / b))/]

then reconsider b = b as zero Real ;
( a / b = 0 & [\a/] / b = 0 & (frac a) / b = 0 ) ;
hence [\(a / b)/] = [\([\a/] / b)/] + [\((frac ([\a/] / b)) + ((frac a) / b))/] ; :: thesis: verum

end;

suppose b <> 0 ; :: thesis: [\(a / b)/] = [\([\a/] / b)/] + [\((frac ([\a/] / b)) + ((frac a) / b))/]

then reconsider b = b as non zero Real ;
[\(a / b)/] = [\(([\a/] + (frac a)) / b)/] by INT_1:42
.= [\(([\a/] / b) + ((frac a) / b))/]
.= [\(([\([\a/] / b)/] + (frac ([\a/] / b))) + ((frac a) / b))/] by INT_1:42
.= [\([\([\a/] / b)/] + ((frac ([\a/] / b)) + ((frac a) / b)))/]
.= [\([\a/] / b)/] + [\((frac ([\a/] / b)) + ((frac a) / b))/] by INT_1:28 ;
hence [\(a / b)/] = [\([\a/] / b)/] + [\((frac ([\a/] / b)) + ((frac a) / b))/] ; :: thesis: verum

end;

end;