set f = Euler_factorization_2 n;
let r be Real; :: according to PARTFUN3:def 1 :: thesis: ( not r in proj2 (Euler_factorization_2 n) or not r <= 0 )
assume r in rng (Euler_factorization_2 n) ; :: thesis: not r <= 0
then consider x being object such that
A2: x in dom (Euler_factorization_2 n) and
A3: (Euler_factorization_2 n) . x = r by FUNCT_1:def 3;
reconsider p = x as Prime by A2, Th29;
(Euler_factorization_2 n) . p = p - 1 by A2, Def3;
hence not r <= 0 by A3; :: thesis: verum