let i, n be Element of NAT ; :: thesis: ( i is_expressible_by n implies MUL_MOD 1,i,n = i )
A1: ChangeVal_1 1,n = 1 by Def7;
assume i is_expressible_by n ; :: thesis: MUL_MOD 1,i,n = i
then A2: i < 2 to_power n by Def3;

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

suppose A3: i = 0 ; :: thesis: MUL_MOD 1,i,n = i

then ChangeVal_1 i,n = 2 to_power n by Def7;
then (ChangeVal_1 i,n) mod ((2 to_power n) + 1) = 2 to_power n by NAT_D:24, XREAL_1:31;
hence MUL_MOD 1,i,n = i by A1, A3, Def8; :: thesis: verum

end;

suppose A4: i <> 0 ; :: thesis: MUL_MOD 1,i,n = i

2 to_power n < (2 to_power n) + 1 by XREAL_1:31;
then A5: i < (2 to_power n) + 1 by A2, XXREAL_0:2;
(ChangeVal_1 i,n) mod ((2 to_power n) + 1) = i mod ((2 to_power n) + 1) by A4, Def7;
then (ChangeVal_1 i,n) mod ((2 to_power n) + 1) = i by A5, NAT_D:24;
hence MUL_MOD 1,i,n = i by A2, A1, Def8; :: thesis: verum

end;

end;