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: 1 < p by INT_2:def 5;
h in Segm0 p ;
then A3: h in (Segm p) \ {0 } by A2, Def2;
not h in {0 } by A3, XBOOLE_0:def 5;
then A4: hp <> 0 by A1, TARSKI:def 1;
0 in Segm p by GR_CY_1:10;
then A5: hp <> 0. (INT.Ring p) by A4, FUNCT_7:def 1;
set hpd = hp " ;
A6: hp * (hp " ) = 1. (INT.Ring p) by A5, VECTSP_1:def 22;
hp " <> 0. (INT.Ring p) by A6, VECTSP_1:36;
then hp " <> 0 by FUNCT_7:def 1;
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 A2, Def2;
h * g = hp * (hp " ) by A1, Lm12
.= 1. (INT.Ring p) by A5, VECTSP_1:def 22
.= 1_ (Z/Z* p) by Th21 ;
hence h " = hp " by GROUP_1:def 6; :: thesis: verum