a mod b in NAT by INT_1:3;
then reconsider x = a mod b as Nat ;
A1: b * c >= b * 1 by XREAL_1:64, NAT_1:14;
a mod b < b by NAT_D:62;
then a mod b < b * c by A1, XXREAL_0:2;
hence (a mod b) mod (b * c) = a mod b by NAT_D:24; :: thesis: verum