let n be Nat; :: thesis: for i being Integer holds n div (n gcd i) = n / (n gcd i)
let i be Integer; :: thesis: n div (n gcd i) = n / (n gcd i)
( i gcd n divides i & i gcd n divides n ) by INT_2:def 2;
hence n div (n gcd i) = n / (n gcd i) by Th6; :: thesis: verum