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

(SMoebius A) . x = (EmptyBag NAT) . x

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

for x being object st x in NAT holds
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;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

(SMoebius A) . x = (EmptyBag NAT) . x

proof

hence
SMoebius A = EmptyBag NAT
by PBOOLE:3; :: thesis: verum
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;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