let k, m, n be Nat; :: thesis: ( m <> 0 implies (k mod (m * n)) mod n = k mod n )
assume A1: m <> 0 ; :: thesis: (k mod (m * n)) mod n = k mod n

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

suppose A2: n <> 0 ; :: thesis: (k mod (m * n)) mod n = k mod n

reconsider k9 = k, m9 = m, n9 = n as Integer ;
m9 * n9 <> 0 by A1, A2, XCMPLX_1:6;
hence (k mod (m * n)) mod n = (k9 - ((k9 div (m9 * n9)) * (m9 * n9))) mod n9 by INT_1:def 10
.= (k9 + ((- (m9 * (k9 div (m9 * n9)))) * n9)) mod n9
.= k mod n by NAT_D:61 ;
:: thesis: verum

end;

suppose A3: n = 0 ; :: thesis: (k mod (m * n)) mod n = k mod n

hence (k mod (m * n)) mod n = 0 by NAT_D:def 2
.= k mod n by A3, NAT_D:def 2 ;
:: thesis: verum

end;

end;