let a, b be non zero Integer; :: thesis: for c being Integer holds (c mod (a * b)) mod a = c mod a
let c be Integer; :: thesis: (c mod (a * b)) mod a = c mod a
A1: c mod (a * b) = (a * b) * (frac (c / (a * b))) by R3;
then reconsider t = (a * b) * (frac (c / (a * b))) as Integer ;
(c mod (a * b)) mod a = a * (frac ((a * (b * (frac (c / (a * b))))) / a)) by A1, R3
.= a * (frac (b * (frac (c / (a * b))))) by XCMPLX_1:89
.= a * (frac (b * (c / (a * b)))) by FR3
.= a * (frac ((b * c) / (a * b))) by XCMPLX_1:74
.= a * (frac (c / a)) by XCMPLX_1:91 ;
hence (c mod (a * b)) mod a = c mod a by R3; :: thesis: verum