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 ;
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 ;
then i <= m by FINSEQ_1:1;
then A6: i <= len f by ;
1 <= i by ;
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 ;
A12: f . j = fm . j by ;
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 ;
then f . i > 0 by PARTFUN3:def 1;
hence r > 0 by ; :: thesis: verum
end;
hence f | m is CR_Sequence by ; :: thesis: verum