set g = - f;
let i, j be Nat; :: according to INT_6:def 2 :: thesis: ( not i in proj1 (- f) or not j in proj1 (- f) or i = j or (- f) . i,(- f) . j are_coprime )
A1: dom (- f) = dom f by VALUED_1:8;
( (- f) . i = - (f . i) & (- f) . j = - (f . j) ) by VALUED_1:8;
hence ( not i in proj1 (- f) or not j in proj1 (- f) or i = j or (- f) . i,(- f) . j are_coprime ) by A1, Th11, INT_6:def 2; :: thesis: verum