set f = Euler_factorization n;
let p be object ; :: according to VALUED_0:def 12 :: thesis: ( not p in proj1 (Euler_factorization n) or (Euler_factorization n) . p is natural )
assume A1: p in dom (Euler_factorization n) ; :: thesis: (Euler_factorization n) . p is natural
then reconsider p = p as Prime by Th17;
consider c being non zero Nat such that
A2: ( c = p |-count n & (Euler_factorization n) . p = (p |^ c) - (p |^ (c - 1)) ) by A1, Def1;
c - 1 <= c - 0 by XREAL_1:7;
then (p |^ c) - (p |^ (c - 1)) in NAT by INT_1:5, NAT_6:1;
hence (Euler_factorization n) . p is natural by A2; :: thesis: verum