let n be Nat; :: thesis: ( n is square-free implies Moebius n <> 0 )
assume n is square-free ; :: thesis: Moebius n <> 0
then consider n9 being non zero Nat such that
A1: ( n9 = n & Moebius n = (- 1) |^ (card (support (ppf n9))) ) by Def3;
Moebius n = (- 1) |^ (card (support (ppf n9))) by A1;
hence Moebius n <> 0 by CARD_4:3; :: thesis: verum