let a be Nat; :: thesis: ( ( a is square & a is square-free ) iff a = 1 )
A1: ( a is square & a is square-free implies a = 1 )

proof

assume B1: ( a is square & a is square-free ) ; :: thesis: a = 1
then reconsider k = 2 -root a as Element of NAT by INT_1:3;
a < 2

proof

assume a >= 2 ; :: thesis: contradiction
then consider p being Element of NAT such that
C1: ( p is prime & p divides a ) by INT_2:31;
not p |^ 2 divides k |^ 2 by B1, C1, MOEBIUS1:def 1;
hence contradiction by NAT_3:5, WSIERP_1:14, C1; :: thesis: verum

end;

hence a = 1 by B1, MOEBIUS1:21, NAT_1:23; :: thesis: verum

end;

( 1 * 1 is square-free & 1 * 1 is square ) by MOEBIUS1:22;
hence ( ( a is square & a is square-free ) iff a = 1 ) by A1; :: thesis: verum