let j be Integer; :: thesis: ( j <> 0 implies for n being positive Nat st ( for i being Nat st i in dom (PrimeDivisorsFS n) holds
j,(PrimeDivisorsFS n) . i are_coprime ) holds
j,n are_coprime )
assume j <> 0 ; :: thesis: for n being positive Nat st ( for i being Nat st i in dom (PrimeDivisorsFS n) holds
j,(PrimeDivisorsFS n) . i are_coprime ) holds
j,n are_coprime
then reconsider j1 = |.j.| as non zero Nat ;
let n be positive Nat; :: thesis: ( ( for i being Nat st i in dom (PrimeDivisorsFS n) holds
j,(PrimeDivisorsFS n) . i are_coprime ) implies j,n are_coprime )
set X = PrimeDivisors n;
set q = PrimeDivisorsFS n;
assume A1: for i being Nat st i in dom (PrimeDivisorsFS n) holds
j,(PrimeDivisorsFS n) . i are_coprime ; :: thesis: j,n are_coprime
set N = ppf n;
set J = ppf j1;

A2: now :: thesis: not support (ppf j1) meets support (ppf n)

assume support (ppf j1) meets support (ppf n) ; :: thesis: contradiction
then consider y being object such that
A3: y in support (ppf j1) and
A4: y in support (ppf n) by XBOOLE_0:3;
set C = canFS (support (ppf n));
PrimeDivisorsFS n = sort_a (canFS (support (ppf n))) by Th52;
then A5: rng (canFS (support (ppf n))) = rng (PrimeDivisorsFS n) by CLASSES1:75, RFINSEQ2:def 6;
support (ppf n) = support (pfexp n) by NAT_3:def 9;
then reconsider y = y as Prime by A4, NAT_3:34;
support (ppf j1) = support (pfexp j1) by NAT_3:def 9;
then A6: y divides j1 by A3, NAT_3:36;
rng (canFS (support (ppf n))) = support (ppf n) by FUNCT_2:def 3;
then consider x being object such that
A7: x in dom (PrimeDivisorsFS n) and
A8: (PrimeDivisorsFS n) . x = y by A4, A5, FUNCT_1:def 3;
j,(PrimeDivisorsFS n) . x are_coprime by A1, A7;
hence contradiction by A6, A8, Th10, PYTHTRIP:def 2; :: thesis: verum

end;

( Product (ppf n) = n & Product (ppf j1) = j1 ) by NAT_3:61;
hence j,n are_coprime by A2, Th10, INT_7:12; :: thesis: verum