let p be Prime; :: thesis: for x being Element of (Z/Z* p)
for x1 being Element of (INT.Ring p) st x = x1 holds
x " = x1 "
let h be Element of (Z/Z* p); :: thesis: for x1 being Element of (INT.Ring p) st h = x1 holds
h " = x1 "
let hp be Element of (INT.Ring p); :: thesis: ( h = hp implies h " = hp " )
assume A1: h = hp ; :: thesis: h " = hp "
A2: 0 in Segm p by NAT_1:44;
set hpd = hp " ;
A3: 1 < p by INT_2:def 4;
h in Segm0 p ;
then h in (Segm p) \ {0} by A3, Def2;
then not h in {0} by XBOOLE_0:def 5;
then hp <> 0 by A1, TARSKI:def 1;
then A4: hp <> 0. (INT.Ring p) by A2, SUBSET_1:def 8;
then hp * (hp ") = 1. (INT.Ring p) by VECTSP_1:def 10;
then hp " <> 0. (INT.Ring p) ;
then hp " <> 0 ;
then not hp " in {0} by TARSKI:def 1;
then hp " in (Segm p) \ {0} by XBOOLE_0:def 5;
then reconsider g = hp " as Element of (Z/Z* p) by A3, Def2;
h * g = hp * (hp ") by A1, Lm12
.= 1. (INT.Ring p) by A4, VECTSP_1:def 10
.= 1_ (Z/Z* p) by Th21 ;
hence h " = hp " by GROUP_1:def 5; :: thesis: verum