let p be Prime; :: thesis: for n being non zero Nat holds Euler_factorization (p |^ n) = p .--> ((p |^ n) - (p |^ (n - 1)))
let n be non zero Nat; :: thesis: Euler_factorization (p |^ n) = p .--> ((p |^ n) - (p |^ (n - 1)))
set x = (p |^ n) - (p |^ (n - 1));
set f = Euler_factorization (p |^ n);
set g = p .--> ((p |^ n) - (p |^ (n - 1)));
A1: dom (Euler_factorization (p |^ n)) = support (ppf (p |^ n)) by Def1
.= support (pfexp (p |^ n)) by NAT_3:def 9
.= {p} by NAT_3:42 ;
A2: dom (p .--> ((p |^ n) - (p |^ (n - 1)))) = {p} ;
A3: p |-count (p |^ n) = n by NAT_3:25, INT_2:def 4;
p in {p} by TARSKI:def 1;
then consider c being non zero Nat such that
A4: ( c = p |-count (p |^ n) & (Euler_factorization (p |^ n)) . p = (p |^ c) - (p |^ (c - 1)) ) by A1, Def1;

now :: thesis: for a being object st a in dom (Euler_factorization (p |^ n)) holds
(Euler_factorization (p |^ n)) . a = (p .--> ((p |^ n) - (p |^ (n - 1)))) . a

let a be object ; :: thesis: ( a in dom (Euler_factorization (p |^ n)) implies (Euler_factorization (p |^ n)) . a = (p .--> ((p |^ n) - (p |^ (n - 1)))) . a )
assume a in dom (Euler_factorization (p |^ n)) ; :: thesis: (Euler_factorization (p |^ n)) . a = (p .--> ((p |^ n) - (p |^ (n - 1)))) . a
then a = p by A1, TARSKI:def 1;
hence (Euler_factorization (p |^ n)) . a = (p .--> ((p |^ n) - (p |^ (n - 1)))) . a by A3, A4, FUNCOP_1:72; :: thesis: verum

end;

hence Euler_factorization (p |^ n) = p .--> ((p |^ n) - (p |^ (n - 1))) by A1, A2, FUNCT_1:def 11; :: thesis: verum