let a1, a2 be Nat; :: thesis: ( MUL_MOD (i,a1,n) = 1 & a1 is_expressible_by n & MUL_MOD (i,a2,n) = 1 & a2 is_expressible_by n implies a1 = a2 )
assume that
A20: MUL_MOD (i,a1,n) = 1 and
A21: a1 is_expressible_by n and
A22: MUL_MOD (i,a2,n) = 1 and
A23: a2 is_expressible_by n ; :: thesis: a1 = a2
consider b2 being Nat such that
A24: b2 = ChangeVal_1 (a2,n) ;
b2 <= 2 to_power n by A23, A24, Th17;
then A25: b2 < (2 to_power n) + 1 by NAT_1:13;
consider b1 being Nat such that
A26: b1 = ChangeVal_1 (a1,n) ;
b1 <= 2 to_power n by A21, A26, Th17;
then A27: b1 < (2 to_power n) + 1 by NAT_1:13;
consider k being Nat such that
A28: k = ChangeVal_1 (i,n) ;
A29: k <= 2 to_power n by A1, A28, Th17;
then A30: k < (2 to_power n) + 1 by NAT_1:13;
A31: k > 0 by A1, A28, Th17;
b2 > 0 by A23, A24, Th17;
then A32: (k * b2) mod ((2 to_power n) + 1) <> 0 by A2, A31, A30, A25, Th5;
b1 > 0 by A21, A26, Th17;
then (k * b1) mod ((2 to_power n) + 1) <> 0 by A2, A31, A30, A27, Th5;
then A33: (k * b1) mod ((2 to_power n) + 1) = (k * b2) mod ((2 to_power n) + 1) by A20, A22, A28, A26, A24, A32, Th20;

now :: thesis: b1 = b2

per cases ( b1 <= b2 or b2 <= b1 ) ;

suppose A34: b1 <= b2 ; :: thesis: b1 = b2

consider b being Integer such that
A35: b = b2 - b1 ;
b1 - b1 <= b2 - b1 by A34, XREAL_1:9;
then reconsider b = b as Element of NAT by A35, INT_1:3;
ex t being Nat st (k * b2) - (k * b1) = ((2 to_power n) + 1) * t by A33, A34, Th2, NAT_1:4;
then (2 to_power n) + 1 divides k * b by A35, NAT_D:def 3;
then A36: ( (2 to_power n) + 1 divides k or (2 to_power n) + 1 divides b ) by A2, NEWTON:80;
b <= 2 to_power n by A23, A24, A35, Th4, Th17;
then A37: not (2 to_power n) + 1 <= b by NAT_1:13;
not (2 to_power n) + 1 <= k by A29, NAT_1:13;
then not 0 < b by A31, A36, A37, NAT_D:7;
then (b2 - b1) + b1 = 0 + b1 by A35;
hence b1 = b2 ; :: thesis: verum

end;

suppose A38: b2 <= b1 ; :: thesis: b2 = b1

consider b being Integer such that
A39: b = b1 - b2 ;
b2 - b2 <= b1 - b2 by A38, XREAL_1:9;
then reconsider b = b as Element of NAT by A39, INT_1:3;
ex t being Nat st (k * b1) - (k * b2) = ((2 to_power n) + 1) * t by A33, A38, Th2, NAT_1:4;
then (2 to_power n) + 1 divides k * b by A39, NAT_D:def 3;
then A40: ( (2 to_power n) + 1 divides k or (2 to_power n) + 1 divides b ) by A2, NEWTON:80;
b <= 2 to_power n by A21, A26, A39, Th4, Th17;
then A41: not (2 to_power n) + 1 <= b by NAT_1:13;
not (2 to_power n) + 1 <= k by A29, NAT_1:13;
then not 0 < b by A31, A40, A41, NAT_D:7;
then (b1 - b2) + b2 = 0 + b2 by A39;
hence b2 = b1 ; :: thesis: verum

end;

end;

end;

hence a1 = a2 by A21, A23, A26, A24, Th18; :: thesis: verum