let n be non zero Nat; :: thesis: Seg (SquarefreePart n) c= Seg n
n = (SquarefreePart n) * ((SqF n) ^2) by Canonical;
then SquarefreePart n divides n ;
then SquarefreePart n <= n by NAT_D:7;
hence Seg (SquarefreePart n) c= Seg n by FINSEQ_1:5; :: thesis: verum