let i2, i3, i1 be Integer; :: thesis: ( i2 > 0 & i3 >= 0 implies (i1 mod (i2 * i3)) mod i3 = i1 mod i3 )
assume A1: ( i2 > 0 & i3 >= 0 ) ; :: thesis: (i1 mod (i2 * i3)) mod i3 = i1 mod i3

per cases ( i3 > 0 or i3 = 0 ) by A1;

suppose i3 > 0 ; :: thesis: (i1 mod (i2 * i3)) mod i3 = i1 mod i3

then i2 * i3 <> 0 by A1, XCMPLX_1:6;
then (i1 mod (i2 * i3)) mod i3 = (i1 - ((i1 div (i2 * i3)) * (i2 * i3))) mod i3 by INT_1:def 8
.= (i1 + ((- (i2 * (i1 div (i2 * i3)))) * i3)) mod i3 ;
hence (i1 mod (i2 * i3)) mod i3 = i1 mod i3 by EULER_1:13; :: thesis: verum

end;

suppose A2: i3 = 0 ; :: thesis: (i1 mod (i2 * i3)) mod i3 = i1 mod i3

then (i1 mod (i2 * i3)) mod i3 = 0 by INT_1:def 8;
hence (i1 mod (i2 * i3)) mod i3 = i1 mod i3 by A2, INT_1:def 8; :: thesis: verum

end;

end;