let k, n be non zero Nat; :: thesis: ( ( k divides n & k is square-free ) iff k divides Radical n )
( k divides Radical n implies ( k divides n & k is square-free ) )

proof

assume A2: k divides Radical n ; :: thesis: ( k divides n & k is square-free )
Radical n divides n by Th55;
hence ( k divides n & k is square-free ) by A2, Th26, NAT_D:4; :: thesis: verum

end;

hence ( ( k divides n & k is square-free ) iff k divides Radical n ) by Lm5; :: thesis: verum