reconsider J = 1 as Element of NAT ;
reconsider M = ({1},1) -bag as Rbag of NAT ;
A1: 1 in {1} by TARSKI:def 1;
A2: 1 in SCNAT by Def2, Th22;
J in {1} by TARSKI:def 1;
then J in {1} /\ SCNAT by A2, XBOOLE_0:def 4;
then J in support (SMoebius {1}) by Def5;
then A3: (SMoebius {1}) . 1 = 1 by Def5, Th30;
{1} c= SCNAT by A2, ZFMISC_1:31;
then A4: {1} /\ SCNAT = {1} by XBOOLE_1:28;
for x being object st x in NAT holds
(SMoebius {1}) . x = M . x
proof
let x be object ; :: thesis: ( x in NAT implies (SMoebius {1}) . x = M . x )
per cases ( x in {1} or not x in {1} ) ;
suppose A5: 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 A3, A5, UPROOTS:7; :: thesis: verum
end;
suppose A6: not x in {1} ; :: thesis: ( x in NAT implies (SMoebius {1}) . x = M . x )
then A7: not x in support (SMoebius {1}) by A4, Def5;
M . x = 0 by A6, UPROOTS:6
.= (SMoebius {1}) . x by A7, PRE_POLY:def 7 ;
hence ( x in NAT implies (SMoebius {1}) . x = M . x ) ; :: thesis: verum
end;
end;
end;
then ( support M = {1} & SMoebius {1} = M ) by PBOOLE:3, UPROOTS:8;
then Sum (SMoebius (NatDivisors 1)) = M . 1 by Th12, Th41
.= 1 by A1, UPROOTS:7 ;
hence Sum (SMoebius (NatDivisors 1)) = 1 ; :: thesis: verum