let f be CR_Sequence; :: thesis: for m being natural number st 0 < m & m <= len f holds
f | m is CR_Sequence
let m be natural number ; :: thesis: ( 0 < m & m <= len f implies f | m is CR_Sequence )
assume AS: ( m > 0 & m <= len f ) ; :: thesis: f | m is CR_Sequence
reconsider fm = f | m as FinSequence of INT by intint;
C: len fm = m by AS, FINSEQ_1:80;

H: now

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 i in Seg m by C, FINSEQ_1:def 3;
then ( 1 <= i & i <= m ) by FINSEQ_1:3;
then ( 1 <= i & i <= len f ) by AS, XXREAL_0:2;
then i in Seg (len f) ;
hence i in dom f by FINSEQ_1:def 3; :: thesis: verum

end;

B: now

let r be real number ; :: thesis: ( r in rng fm implies r > 0 )
assume r in rng fm ; :: thesis: r > 0
then consider i being set such that
B0: ( i in dom fm & fm . i = r ) by FUNCT_1:def 5;
reconsider i = i as Element of NAT by B0;
f . i in rng f by H, B0, FUNCT_1:12;
then f . i > 0 by PARTFUN3:def 1;
hence r > 0 by B0, FUNCT_1:70; :: thesis: verum

end;

now

let i', j' be natural number ; :: thesis: ( i' in dom fm & j' in dom fm & i' <> j' implies fm . i',fm . j' are_relative_prime )
assume B1: ( i' in dom fm & j' in dom fm & i' <> j' ) ; :: thesis: fm . i',fm . j' are_relative_prime
reconsider i = i', j = j' as Element of NAT by ORDINAL1:def 13;
B2: ( i in dom f & j in dom f ) by H, B1;
B4: f . i = fm . i by B1, FUNCT_1:70;
f . j = fm . j by B1, FUNCT_1:70;
hence fm . i',fm . j' are_relative_prime by B1, B2, B4, DefCR; :: thesis: verum

end;

hence f | m is CR_Sequence by B, C, DefCR, AS, FINSEQ_1:def 3, PARTFUN3:def 1; :: thesis: verum