let i, j be Nat; :: according to INT_6:def 2 :: thesis: ( not i in proj1 (Sgm X) or not j in proj1 (Sgm X) or i = j or (Sgm X) . i,(Sgm X) . j are_coprime )
assume A2: i in dom (Sgm X) ; :: thesis: ( not j in proj1 (Sgm X) or i = j or (Sgm X) . i,(Sgm X) . j are_coprime )
then A3: (Sgm X) . i in rng (Sgm X) by FUNCT_1:def 3;
assume A4: j in dom (Sgm X) ; :: thesis: ( i = j or (Sgm X) . i,(Sgm X) . j are_coprime )
then A5: (Sgm X) . j in rng (Sgm X) by FUNCT_1:def 3;
A6: ( 1 <= i & i <= len (Sgm X) ) by A2, FINSEQ_3:25;
A7: ( 1 <= j & j <= len (Sgm X) ) by A4, FINSEQ_3:25;
assume i <> j ; :: thesis: (Sgm X) . i,(Sgm X) . j are_coprime
then ( i < j or i > j ) by XXREAL_0:1;
then A8: ( (Sgm X) . i < (Sgm X) . j or (Sgm X) . i > (Sgm X) . j ) by A6, A7, FINSEQ_1:def 14;
( (Sgm X) . i is prime & (Sgm X) . j is prime ) by A1, A3, A5, NEWTON:def 6;
hence (Sgm X) . i,(Sgm X) . j are_coprime by A8, INT_2:30; :: thesis: verum