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;

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

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

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

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

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

r > 0

hence
f | m is CR_Sequence
by A1, A3, A7, Def2, PARTFUN3:def 1; :: thesis: verumr > 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;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