let n be non zero Nat; :: thesis: Euler_factorization_2 n <= n - 1
set f = Euler_factorization_2 n;
let x be object ; :: according to NUMBER08:def 4 :: thesis: ( x in dom (Euler_factorization_2 n) implies (Euler_factorization_2 n) . x <= n - 1 )
assume A1: x in dom (Euler_factorization_2 n) ; :: thesis: (Euler_factorization_2 n) . x <= n - 1
reconsider p = x as Prime by A1, Th29;
A2: (Euler_factorization_2 n) . p = p - 1 by A1, Def3;
A3: support (ppf n) = support (pfexp n) by NAT_3:def 9;
dom (Euler_factorization_2 n) = support (ppf n) by Def3;
then p <= n by A1, A3, NAT_3:36, NAT_D:7;
hence (Euler_factorization_2 n) . x <= n - 1 by A2, XREAL_1:7; :: thesis: verum