let n be non zero Nat; :: thesis: ( n > 1 implies not support (Euler_factorization n) is empty )
assume A1: n > 1 ; :: thesis: not support (Euler_factorization n) is empty
set f = Euler_factorization n;
n >= 1 + 1 by A1, NAT_1:13;
then consider p being Element of NAT such that
A2: p is prime and
A3: p divides n by INT_2:31;
dom (Euler_factorization n) = support (ppf n) by Def1
.= support (pfexp n) by NAT_3:def 9 ;
then consider c being non zero Nat such that
A4: ( c = p |-count n & (Euler_factorization n) . p = (p |^ c) - (p |^ (c - 1)) ) by A2, A3, NAT_3:37, Def1;
c - 1 < c - 0 by XREAL_1:15;
then (Euler_factorization n) . p <> 0 by A2, A4, NAT_6:2;
hence not support (Euler_factorization n) is empty by PRE_POLY:def 7; :: thesis: verum