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

proof

assume A1: not n is square-containing ; :: thesis: ex n9 being non zero natural number st
( n9 = n & ex r being real number st r = (- 1) |^ (card (support (ppf n9))) )
n is non zero natural number

proof

consider p being Prime;
assume n is not non zero natural number ; :: thesis: contradiction
then p |^ 2 divides n by NAT_D:6;
hence contradiction by A1, Def1; :: thesis: verum

end;

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

end;

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