let k be natural number ; :: thesis: sigma k,1 = 1
set b = (EXP k) | (NatDivisors 1);
A1: support ((EXP k) | (NatDivisors 1)) c= dom ((EXP k) | (NatDivisors 1)) by POLYNOM1:41;
1 in NAT ;
then A2: 1 in dom (EXP k) by FUNCT_2:def 1;
1 in NatDivisors 1 ;
then A3: 1 in dom ((EXP k) | (NatDivisors 1)) by A2, RELAT_1:86;
A4: ((EXP k) | (NatDivisors 1)) . 1 = (EXP k) . 1 by A3, FUNCT_1:70
.= 1 |^ k by Def1
.= 1 by NEWTON:15 ;
for x being set holds
( x in support ((EXP k) | (NatDivisors 1)) iff x = 1 )

proof

let x be set ; :: thesis: ( x in support ((EXP k) | (NatDivisors 1)) iff x = 1 )

hereby :: thesis: ( x = 1 implies x in support ((EXP k) | (NatDivisors 1)) )

assume x in support ((EXP k) | (NatDivisors 1)) ; :: thesis: x = 1
then x in NatDivisors 1 by A1, RELAT_1:86;
hence x = 1 by TARSKI:def 1, MOEBIUS1:41; :: thesis: verum

end;

assume x = 1 ; :: thesis: x in support ((EXP k) | (NatDivisors 1))
hence x in support ((EXP k) | (NatDivisors 1)) by A4, POLYNOM1:def 7; :: thesis: verum

end;

then A5: support ((EXP k) | (NatDivisors 1)) = {1} by TARSKI:def 1;
consider f being FinSequence of REAL such that
A6: ( Sum ((EXP k) | (NatDivisors 1)) = Sum f & f = ((EXP k) | (NatDivisors 1)) * (canFS (support ((EXP k) | (NatDivisors 1)))) ) by UPROOTS:def 3;
f = ((EXP k) | (NatDivisors 1)) * <*1*> by A6, A5, UPROOTS:6
.= <*(((EXP k) | (NatDivisors 1)) . 1)*> by A3, BAGORDER:3 ;
then A7: Sum ((EXP k) | (NatDivisors 1)) = 1 by A6, A4, RVSUM_1:103;
thus sigma k,1 = 1 by A7, Def2; :: thesis: verum