let n be Nat; :: thesis: ( n is prime implies Euler n = n - 1 )
set X = { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ;
{ kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } c= Seg n

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } or x in Seg n )
assume x in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ; :: thesis: x in Seg n
then ex k being Element of NAT st
( k = x & n,k are_coprime & k >= 1 & k <= n ) ;
hence x in Seg n by FINSEQ_1:1; :: thesis: verum

end;

then reconsider X = { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } as finite set ;
assume A1: n is prime ; :: thesis: Euler n = n - 1
n <> 0

proof

assume n = 0 ; :: thesis: contradiction
then n in SetPrimenumber 2 by A1, NEWTON:def 7;
hence contradiction ; :: thesis: verum

end;

then 0 in { l where l is Nat : l < n } ;
then A2: 0 in n by AXIOMS:4;
(Segm n) \ {0} c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Segm n) \ {0} or x in X )
assume A3: x in (Segm n) \ {0} ; :: thesis: x in X
then A4: x in Segm n by XBOOLE_0:def 5;
not x in {0} by A3, XBOOLE_0:def 5;
hence x in X by A1, Th3, A4; :: thesis: verum

end;

then A5: card (n \ {0}) <= card X by NAT_1:43;
A6: Euler n <= n - 1 by A1, Th19, INT_2:def 4;
( card n = n & card {0} = 1 ) by CARD_1:30;
then n - 1 <= Euler n by A5, A2, Th4;
hence Euler n = n - 1 by A6, XXREAL_0:1; :: thesis: verum