set f = Euler_factorization_2 n;
let p be object ; :: according to VALUED_0:def 12 :: thesis: ( not p in proj1 (Euler_factorization_2 n) or (Euler_factorization_2 n) . p is natural )
assume A1: p in dom (Euler_factorization_2 n) ; :: thesis: (Euler_factorization_2 n) . p is natural
then reconsider p = p as Prime by Th29;
(Euler_factorization_2 n) . p = p - 1 by A1, Def3;
hence (Euler_factorization_2 n) . p is natural ; :: thesis: verum