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 n' being non zero natural number st
( n' = n & b₁ = (- 1) |^ (card (support (ppf n'))) ) )
( not n is square-containing implies ex n' being non zero natural number st
( n' = n & ex r being real number st r = (- 1) |^ (card (support (ppf n'))) ) )

proof

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

proof

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

end;

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

end;

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