set g = f (#) f;
let i, j be Nat; :: according to INT_6:def 2 :: thesis: ( not i in proj1 (f (#) f) or not j in proj1 (f (#) f) or i = j or (f (#) f) . i,(f (#) f) . j are_coprime )
assume that
A1: ( i in dom (f (#) f) & j in dom (f (#) f) ) and
A2: i <> j ; :: thesis: (f (#) f) . i,(f (#) f) . j are_coprime
A3: dom (f (#) f) = (dom f) /\ (dom f) by VALUED_1:def 4;
then A4: ( f . i <> 0 & f . j <> 0 ) by A1, FUNCT_1:def 9;
f . i,f . j are_coprime by A1, A2, A3, INT_6:def 2;
then A5: (f . i) * (f . i),f . j are_coprime by A4, Th16;
( (f (#) f) . i = (f . i) * (f . i) & (f (#) f) . j = (f . j) * (f . j) ) by VALUED_1:5;
hence (f (#) f) . i,(f (#) f) . j are_coprime by A4, A5, Th16; :: thesis: verum