let n, s be Nat; :: thesis: for p being Prime st Sum (canFS (NatDivisors p)) = n |^ s & 2 <= s holds
n = 2
let p be Prime; :: thesis: ( Sum (canFS (NatDivisors p)) = n |^ s & 2 <= s implies n = 2 )
assume A1: ( Sum (canFS (NatDivisors p)) = n |^ s & s >= 2 ) ; :: thesis: n = 2
A2: p <> 1 by INT_2:def 4;
NatDivisors p = {1,p} by LATSTONE:26;
then ( canFS (NatDivisors p) = <*1,p*> or canFS (NatDivisors p) = <*p,1*> ) by A2, POLYVIE1:1;
then A3: Sum (canFS (NatDivisors p)) = 1 + p by RVSUM_1:77;
A4: s > 1 by A1, XXREAL_0:2;
n <> 0 by A1, XXREAL_0:2, A3, NEWTON:11;
then A5: ( n >= 1 & n - 1 = n -' 1 ) by NAT_1:14, XREAL_1:233;
p = (n |^ s) - 1 by A3, A1;
then consider m being Nat such that
A6: p = (n -' 1) * m by NAT_D:def 3, A5, NUMBER01:11;
m divides p by A6;

per cases then ( m = 1 or m = p ) by INT_2:def 4;

suppose m = 1 ; :: thesis: n = 2

then n |^ 1 = n |^ s by A3, A6, A5, A1;
then n <= 1 by A4, PEPIN:30;
then n = 1 by A5, XXREAL_0:1;
then n -' 1 = 0 by A5;
hence n = 2 by A6; :: thesis: verum

end;

suppose m = p ; :: thesis: n = 2

then n -' 1 = 1 by A6, XCMPLX_1:7;
hence n = 2 by A5; :: thesis: verum

end;

end;