let n be natural number ; :: thesis: ( not n is square-containing implies Moebius n <> 0 )
assume not n is square-containing ; :: thesis: Moebius n <> 0
then consider n9 being non zero natural number such that
W: ( n9 = n & Moebius n = (- 1) |^ (card (support (ppf n9))) ) by Def3;
Moebius n = (- 1) |^ (card (support (ppf n9))) by W;
hence Moebius n <> 0 by CARD_4:51; :: thesis: verum