let n be non zero Element of NAT ; :: thesis: for A being finite Subset of NAT st A = { k where k is Element of NAT : ( 0 < k & k divides n & k is square-containing ) } holds
SMoebius A = EmptyBag NAT
let A be finite Subset of NAT ; :: thesis: ( A = { k where k is Element of NAT : ( 0 < k & k divides n & k is square-containing ) } implies SMoebius A = EmptyBag NAT )
assume A1: A = { k where k is Element of NAT : ( 0 < k & k divides n & k is square-containing ) } ; :: thesis: SMoebius A = EmptyBag NAT
A2: A misses SCNAT

proof

assume A meets SCNAT ; :: thesis: contradiction
then consider x being set such that
A3: ( x in A & x in SCNAT ) by XBOOLE_0:3;
ex k being Element of NAT st
( k = x & 0 < k & k divides n & k is square-containing ) by A1, A3;
hence contradiction by A3, Def2; :: thesis: verum

end;

for x being set st x in NAT holds
(SMoebius A) . x = (EmptyBag NAT ) . x

proof

let x be set ; :: thesis: ( x in NAT implies (SMoebius A) . x = (EmptyBag NAT ) . x )
assume x in NAT ; :: thesis: (SMoebius A) . x = (EmptyBag NAT ) . x
then reconsider k = x as Element of NAT ;
support (SMoebius A) = A /\ SCNAT by Def5
.= {} by A2, XBOOLE_0:def 7 ;
then (SMoebius A) . k = 0 by POLYNOM1:def 7;
hence (SMoebius A) . x = (EmptyBag NAT ) . x by POLYNOM1:56; :: thesis: verum

end;

hence SMoebius A = EmptyBag NAT by PBOOLE:3; :: thesis: verum