let f be CR_Sequence; for m being Nat st 0 < m & m <= len f holds
f | m is CR_Sequence
let m be Nat; ( 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
; f | m is CR_Sequence
A3:
len fm = m
by A2, FINSEQ_1:59;
A7:
now 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;
( 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
;
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;
verum end;
hence
f | m is CR_Sequence
by A1, A7, Def2, PARTFUN3:def 1; verum