let k be Nat; sigma (k,1) = 1
set b = (EXP k) | (NatDivisors 1);
consider f being FinSequence of REAL such that
A1:
Sum ((EXP k) | (NatDivisors 1)) = Sum f
and
A2:
f = ((EXP k) | (NatDivisors 1)) * (canFS (support ((EXP k) | (NatDivisors 1))))
by UPROOTS:def 3;
1 in NAT
;
then A3:
1 in dom (EXP k)
by FUNCT_2:def 1;
1 in NatDivisors 1
;
then A4:
1 in dom ((EXP k) | (NatDivisors 1))
by A3, RELAT_1:57;
then A5: ((EXP k) | (NatDivisors 1)) . 1 =
(EXP k) . 1
by FUNCT_1:47
.=
1 |^ k
by Def1
.=
1
;
then
for x being object holds
( x in support ((EXP k) | (NatDivisors 1)) iff x = 1 )
by MOEBIUS1:41, TARSKI:def 1, PRE_POLY:def 7;
then
support ((EXP k) | (NatDivisors 1)) = {1}
by TARSKI:def 1;
then f =
((EXP k) | (NatDivisors 1)) * <*1*>
by A2, FINSEQ_1:94
.=
<*(((EXP k) | (NatDivisors 1)) . 1)*>
by A4, FINSEQ_2:34
;
then
Sum ((EXP k) | (NatDivisors 1)) = 1
by A5, A1, RVSUM_1:73;
hence
sigma (k,1) = 1
by Def2; verum