let p be Prime; :: thesis: ( 1_ (Z/Z* p) = 1 & 1_ (Z/Z* p) = 1. (INT.Ring p) )
A1: not 1 in {0} by TARSKI:def 1;
A2: 1 < p by INT_2:def 4;
then 1 in Segm p by NAT_1:44;
then 1 in (Segm p) \ {0} by A1, XBOOLE_0:def 5;
then 1 in Segm0 p by A2, Def2;
then reconsider e = 1. (INT.Ring p) as Element of (Z/Z* p) by A2, INT_3:14;
now :: thesis: for h being Element of (Z/Z* p) holds
( h * e = h & e * h = h )
let h be Element of (Z/Z* p); :: thesis: ( h * e = h & e * h = h )
h in Segm0 p ;
then h in (Segm p) \ {0} by A2, Def2;
then reconsider hp = h as Element of (INT.Ring p) by XBOOLE_0:def 5;
thus h * e = hp * (1_ (INT.Ring p)) by Lm12
.= h ; :: thesis: e * h = h
thus e * h = (1_ (INT.Ring p)) * hp by Lm12
.= h ; :: thesis: verum
end;
then e = 1_ (Z/Z* p) by GROUP_1:def 4;
hence ( 1_ (Z/Z* p) = 1 & 1_ (Z/Z* p) = 1. (INT.Ring p) ) by A2, INT_3:14; :: thesis: verum