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

now

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 A2, 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 A1, Def3; :: 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, Def3; :: thesis: verum

end;

end;

end;

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