let m, k, 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 k' = k, m' = m, n' = n as Integer ;
m' * n' <> 0 by A1, A2, XCMPLX_1:6;
hence (k mod (m * n)) mod n = (k' - ((k' div (m' * n')) * (m' * n'))) mod n' by INT_1:def 8
.= (k' + ((- (m' * (k' div (m' * n')))) * n')) mod n'
.= k mod n by EULER_1:13 ;
:: 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;