set f = Euler_factorization_1 n;
let p be object ; :: according to VALUED_0:def 12 :: thesis: ( not p in proj1 (Euler_factorization_1 n) or (Euler_factorization_1 n) . p is natural )
assume A1: p in dom (Euler_factorization_1 n) ; :: thesis: (Euler_factorization_1 n) . p is natural
then reconsider p = p as Prime by Th27;
ex c being non zero Nat st
( c = p |-count n & (Euler_factorization_1 n) . p = p |^ (c - 1) ) by A1, Def2;
hence (Euler_factorization_1 n) . p is natural ; :: thesis: verum