set p = <*1*>;

now

let u be set ; :: thesis: ( u in {1} implies u in INT )
assume u in {1} ; :: thesis: u in INT
then reconsider u9 = u as Element of NAT by TARSKI:def 1;
u9 is integer number ;
hence u in INT by INT_1:def 1; :: thesis: verum

end;

then {1} c= INT by TARSKI:def 3;
then rng <*1*> c= INT by FINSEQ_1:39;
then reconsider f = <*1*> as FinSequence of INT by FINSEQ_1:def 4;
take f ; :: thesis: ( not f is empty & f is positive-yielding & f is Chinese_Remainder )

A1: now

let i be Element of NAT ; :: thesis: ( i in dom f implies i = 1 )
assume i in dom f ; :: thesis: i = 1
then i in Seg 1 by FINSEQ_1:38;
hence i = 1 by FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;

A2: now

let i9, j9 be natural number ; :: thesis: ( i9 in dom f & j9 in dom f & i9 <> j9 implies f . i9,f . j9 are_relative_prime )
assume that
A3: i9 in dom f and
A4: j9 in dom f and
A5: i9 <> j9 ; :: thesis: f . i9,f . j9 are_relative_prime
reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def 12;
i = 1 by A1, A3
.= j by A1, A4 ;
hence f . i9,f . j9 are_relative_prime by A5; :: thesis: verum

end;

now

let r be real number ; :: thesis: ( r in rng f implies 0 < r )
assume r in rng f ; :: thesis: 0 < r
then r in {1} by FINSEQ_1:39;
hence 0 < r by TARSKI:def 1; :: thesis: verum

end;

hence ( not f is empty & f is positive-yielding & f is Chinese_Remainder ) by A2, Def2, PARTFUN3:def 1; :: thesis: verum