thus ( n is square-containing implies ex r being Real st r = 0 ) ; :: thesis: ( not n is square-containing implies ex b₁ being Real ex n1 being non zero Nat st
( n1 = n & b₁ = (- 1) |^ (card (support (ppf n1))) ) )
( n is square-free implies ex n9 being non zero Nat st
( n9 = n & ex r being Real st r = (- 1) |^ (card (support (ppf n9))) ) )

proof

assume A1: n is square-free ; :: thesis: ex n9 being non zero Nat st
( n9 = n & ex r being Real st r = (- 1) |^ (card (support (ppf n9))) )
n is non zero Nat

proof

set p = the Prime;
assume n is not non zero Nat ; :: thesis: contradiction
then the Prime |^ 2 divides n by NAT_D:6;
hence contradiction by A1; :: thesis: verum

end;

then reconsider n9 = n as non zero Nat ;
ex r being Real st r = (- 1) |^ (card (support (ppf n9))) ;
hence ex n9 being non zero Nat st
( n9 = n & ex r being Real st r = (- 1) |^ (card (support (ppf n9))) ) ; :: thesis: verum

end;

hence ( not n is square-containing implies ex b₁ being Real ex n1 being non zero Nat st
( n1 = n & b₁ = (- 1) |^ (card (support (ppf n1))) ) ) ; :: thesis: verum