let f be CR_Sequence; :: thesis: for m being Nat st 0 < m & m <= len f holds
f | m is CR_Sequence
let m be Nat; :: thesis: ( 0 < m & m <= len f implies f | m is CR_Sequence )
reconsider fm = f | m as FinSequence of INT by Lm1;
assume that
A1: m > 0 and
A2: m <= len f ; :: thesis: f | m is CR_Sequence
A3: len fm = m by A2, FINSEQ_1:59;
A4: now :: thesis: for i being Element of NAT st i in dom fm holds
i in dom f
let i be Element of NAT ; :: thesis: ( i in dom fm implies i in dom f )
assume i in dom fm ; :: thesis: i in dom f
then A5: i in Seg m by A3, FINSEQ_1:def 3;
then i <= m by FINSEQ_1:1;
then A6: i <= len f by A2, XXREAL_0:2;
1 <= i by A5, FINSEQ_1:1;
then i in Seg (len f) by A6;
hence i in dom f by FINSEQ_1:def 3; :: thesis: verum
end;
A7: now :: thesis: for i9, j9 being Nat st i9 in dom fm & j9 in dom fm & i9 <> j9 holds
fm . i9,fm . j9 are_coprime
let i9, j9 be Nat; :: thesis: ( i9 in dom fm & j9 in dom fm & i9 <> j9 implies fm . i9,fm . j9 are_coprime )
assume that
A8: i9 in dom fm and
A9: j9 in dom fm and
A10: i9 <> j9 ; :: thesis: fm . i9,fm . j9 are_coprime
reconsider i = i9, j = j9 as Element of NAT by ORDINAL1:def 12;
A11: f . i = fm . i by A8, FUNCT_1:47;
A12: f . j = fm . j by A9, FUNCT_1:47;
A13: j in dom f by A4, A9;
i in dom f by A4, A8;
hence fm . i9,fm . j9 are_coprime by A10, A13, A11, A12, Def2; :: thesis: verum
end;
now :: thesis: for r being Real st r in rng fm holds
r > 0
let r be Real; :: thesis: ( r in rng fm implies r > 0 )
assume r in rng fm ; :: thesis: r > 0
then consider i being object such that
A14: i in dom fm and
A15: fm . i = r by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A14;
f . i in rng f by A4, A14, FUNCT_1:3;
then f . i > 0 by PARTFUN3:def 1;
hence r > 0 by A14, A15, FUNCT_1:47; :: thesis: verum
end;
hence f | m is CR_Sequence by A1, A7, Def2, PARTFUN3:def 1; :: thesis: verum