let i, j, n be Nat; :: thesis: MUL_MOD (i,j,n) is_expressible_by n
set CV = ((ChangeVal_1 (i,n)) * (ChangeVal_1 (j,n))) mod ((2 to_power n) + 1);
((ChangeVal_1 (i,n)) * (ChangeVal_1 (j,n))) mod ((2 to_power n) + 1) < (2 to_power n) + 1 by NAT_D:1;
then A1: ((ChangeVal_1 (i,n)) * (ChangeVal_1 (j,n))) mod ((2 to_power n) + 1) <= 2 to_power n by NAT_1:13;
A2: 0 < 2 to_power n by POWER:34;

now :: thesis: MUL_MOD (i,j,n) is_expressible_by n

per cases ( ((ChangeVal_1 (i,n)) * (ChangeVal_1 (j,n))) mod ((2 to_power n) + 1) = 2 to_power n or ((ChangeVal_1 (i,n)) * (ChangeVal_1 (j,n))) mod ((2 to_power n) + 1) < 2 to_power n ) by A1, XXREAL_0:1;

suppose ((ChangeVal_1 (i,n)) * (ChangeVal_1 (j,n))) mod ((2 to_power n) + 1) = 2 to_power n ; :: thesis: MUL_MOD (i,j,n) is_expressible_by n

then ChangeVal_2 ((((ChangeVal_1 (i,n)) * (ChangeVal_1 (j,n))) mod ((2 to_power n) + 1)),n) = 0 by Def8;
hence MUL_MOD (i,j,n) is_expressible_by n by A2; :: thesis: verum

end;

suppose A3: ((ChangeVal_1 (i,n)) * (ChangeVal_1 (j,n))) mod ((2 to_power n) + 1) < 2 to_power n ; :: thesis: MUL_MOD (i,j,n) is_expressible_by n

then ChangeVal_2 ((((ChangeVal_1 (i,n)) * (ChangeVal_1 (j,n))) mod ((2 to_power n) + 1)),n) = ((ChangeVal_1 (i,n)) * (ChangeVal_1 (j,n))) mod ((2 to_power n) + 1) by Def8;
hence MUL_MOD (i,j,n) is_expressible_by n by A3; :: thesis: verum

end;

end;

end;

hence MUL_MOD (i,j,n) is_expressible_by n ; :: thesis: verum