let i, n be 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 ;

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:29;
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:29;
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;