A1: for n1, n2 being Element of NAT holds
( ( not n <> 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) & ( n <> 0 & ( for m being non zero Nat st n = m holds
n1 = Sum ((EXP k) | (NatDivisors m)) ) & ( for m being non zero Nat st n = m holds
n2 = Sum ((EXP k) | (NatDivisors m)) ) implies n1 = n2 ) )

proof

let n1, n2 be Element of NAT ; :: thesis: ( ( not n <> 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) & ( n <> 0 & ( for m being non zero Nat st n = m holds
n1 = Sum ((EXP k) | (NatDivisors m)) ) & ( for m being non zero Nat st n = m holds
n2 = Sum ((EXP k) | (NatDivisors m)) ) implies n1 = n2 ) )
thus ( not n <> 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) ; :: thesis: ( n <> 0 & ( for m being non zero Nat st n = m holds
n1 = Sum ((EXP k) | (NatDivisors m)) ) & ( for m being non zero Nat st n = m holds
n2 = Sum ((EXP k) | (NatDivisors m)) ) implies n1 = n2 )
assume n <> 0 ; :: thesis: ( ex m being non zero Nat st
( n = m & not n1 = Sum ((EXP k) | (NatDivisors m)) ) or ex m being non zero Nat st
( n = m & not n2 = Sum ((EXP k) | (NatDivisors m)) ) or n1 = n2 )
then reconsider m = n as non zero Nat by TARSKI:1;
assume for m being non zero Nat st n = m holds
n1 = Sum ((EXP k) | (NatDivisors m)) ; :: thesis: ( ex m being non zero Nat st
( n = m & not n2 = Sum ((EXP k) | (NatDivisors m)) ) or n1 = n2 )
then n1 = Sum ((EXP k) | (NatDivisors m)) ;
hence ( ex m being non zero Nat st
( n = m & not n2 = Sum ((EXP k) | (NatDivisors m)) ) or n1 = n2 ) ; :: thesis: verum

end;

( n <> 0 implies ex n1 being Element of NAT st
for m being non zero Nat st n = m holds
n1 = Sum ((EXP k) | (NatDivisors m)) )

proof

assume n <> 0 ; :: thesis: ex n1 being Element of NAT st
for m being non zero Nat st n = m holds
n1 = Sum ((EXP k) | (NatDivisors m))
then reconsider n9 = n as non zero Nat by TARSKI:1;
reconsider n1 = Sum ((EXP k) | (NatDivisors n9)) as Element of NAT by ORDINAL1:def 12;
take n1 ; :: thesis: for m being non zero Nat st n = m holds
n1 = Sum ((EXP k) | (NatDivisors m))
thus for m being non zero Nat st n = m holds
n1 = Sum ((EXP k) | (NatDivisors m)) ; :: thesis: verum

end;

hence ( ( for b₁ being Element of NAT holds verum ) & ( n <> 0 implies ex b₁ being Element of NAT st
for m being non zero Nat st n = m holds
b₁ = Sum ((EXP k) | (NatDivisors m)) ) & ( not n <> 0 implies ex b₁ being Element of NAT st b₁ = 0 ) & ( for b₁, b₂ being Element of NAT holds
( ( n <> 0 & ( for m being non zero Nat st n = m holds
b₁ = Sum ((EXP k) | (NatDivisors m)) ) & ( for m being non zero Nat st n = m holds
b₂ = Sum ((EXP k) | (NatDivisors m)) ) implies b₁ = b₂ ) & ( not n <> 0 & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) ) ) ) by A1; :: thesis: verum