let m, n be non zero Nat; :: thesis: ( SquarefreePart n = SquarefreePart m & TSqF m = TSqF n implies m = n )
assume A1: ( SquarefreePart n = SquarefreePart m & TSqF m = TSqF n ) ; :: thesis: m = n
m = (SquarefreePart m) * ((SqF m) ^2) by Canonical
.= (SquarefreePart m) * ((SqF m) |^ 2) by NEWTON:81
.= (SquarefreePart n) * (TSqF n) by A1, Cosik
.= (SquarefreePart n) * ((SqF n) |^ 2) by Cosik
.= (SquarefreePart n) * ((SqF n) ^2) by NEWTON:81
.= n by Canonical ;
hence m = n ; :: thesis: verum