A1: 1 in {1} by TARSKI:def 1;
reconsider M = {1},1 -bag as Rbag of ;
A2: support M = {1} by UPROOTS:10;
A3: 1 in SCNAT by Def2, Th22;
then {1} c= SCNAT by ZFMISC_1:37;
then A4: {1} /\ SCNAT = {1} by XBOOLE_1:28;
reconsider J = 1 as Element of NAT ;
J in {1} by TARSKI:def 1;
then J in {1} /\ SCNAT by A3, XBOOLE_0:def 4;
then J in support (SMoebius {1}) by Def5;
then A5: (SMoebius {1}) . 1 = 1 by Def5, Th30;
for x being set st x in NAT holds
(SMoebius {1}) . x = M . x

proof

let x be set ; :: thesis: ( x in NAT implies (SMoebius {1}) . x = M . x )

per cases ( x in {1} or not x in {1} ) ;

suppose A6: x in {1} ; :: thesis: ( x in NAT implies (SMoebius {1}) . x = M . x )

then x = 1 by TARSKI:def 1;
hence ( x in NAT implies (SMoebius {1}) . x = M . x ) by A5, A6, UPROOTS:9; :: thesis: verum

end;

suppose A7: not x in {1} ; :: thesis: ( x in NAT implies (SMoebius {1}) . x = M . x )

then A8: not x in support (SMoebius {1}) by A4, Def5;
M . x = 0 by A7, UPROOTS:8
.= (SMoebius {1}) . x by A8, POLYNOM1:def 7 ;
hence ( x in NAT implies (SMoebius {1}) . x = M . x ) ; :: thesis: verum

end;

end;

end;

then SMoebius {1} = M by PBOOLE:3;
then Sum (SMoebius (NatDivisors 1)) = M . 1 by A2, Th12, Th41
.= 1 by A1, UPROOTS:9 ;
hence Sum (SMoebius (NatDivisors 1)) = 1 ; :: thesis: verum