let p be Prime; :: thesis: Euler_factorization p = p .--> (p - 1)
Euler_factorization (p |^ 1) = p .--> ((p |^ 1) - (p |^ (1 - 1))) by Th19;
hence Euler_factorization p = p .--> (p - 1) by NEWTON:4; :: thesis: verum