let k be Nat; :: thesis: 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; :: thesis: verum

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; :: thesis: verum