set p = <*1*>;

{1} c= INT by Lm7, 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 )

{1} c= INT by Lm7, 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 :: thesis: for i being Element of NAT st i in dom f holds

i = 1

i = 1

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;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

A2: now :: thesis: for i9, j9 being Nat st i9 in dom f & j9 in dom f & i9 <> j9 holds

f . i9,f . j9 are_coprime

f . i9,f . j9 are_coprime

let i9, j9 be Nat; :: thesis: ( i9 in dom f & j9 in dom f & i9 <> j9 implies f . i9,f . j9 are_coprime )

assume that

A3: i9 in dom f and

A4: j9 in dom f and

A5: i9 <> j9 ; :: thesis: f . i9,f . j9 are_coprime

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_coprime by A5; :: thesis: verum

end;assume that

A3: i9 in dom f and

A4: j9 in dom f and

A5: i9 <> j9 ; :: thesis: f . i9,f . j9 are_coprime

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_coprime by A5; :: thesis: verum

now :: thesis: for r being Real st r in rng f holds

0 < r

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

let r be Real; :: 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;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