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 object such that
A3: x in A and
A4: 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 A4, Def2; :: thesis: verum
end;
for x being object st x in NAT holds
(SMoebius A) . x = (EmptyBag NAT) . x
proof
let x be object ; :: 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 ;
then (SMoebius A) . k = 0 by PRE_POLY:def 7;
hence (SMoebius A) . x = (EmptyBag NAT) . x by PBOOLE:5; :: thesis: verum
end;
hence SMoebius A = EmptyBag NAT by PBOOLE:3; :: thesis: verum