A1: for n1, n2 being Element of NAT holds
( ( not n <> 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) & ( n <> 0 & ( for m being natural non zero number st n = m holds
n1 = Sum ((EXP k) | (NatDivisors m)) ) & ( for m being natural non zero number 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 natural non zero number st n = m holds
n1 = Sum ((EXP k) | (NatDivisors m)) ) & ( for m being natural non zero number 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 natural non zero number st n = m holds
n1 = Sum ((EXP k) | (NatDivisors m)) ) & ( for m being natural non zero number st n = m holds
n2 = Sum ((EXP k) | (NatDivisors m)) ) implies n1 = n2 )
assume n <> 0 ; :: thesis: ( ex m being natural non zero number st
( n = m & not n1 = Sum ((EXP k) | (NatDivisors m)) ) or ex m being natural non zero number st
( n = m & not n2 = Sum ((EXP k) | (NatDivisors m)) ) or n1 = n2 )
then reconsider m = n as natural non zero number ;
assume for m being natural non zero number st n = m holds
n1 = Sum ((EXP k) | (NatDivisors m)) ; :: thesis: ( ex m being natural non zero number st
( n = m & not n2 = Sum ((EXP k) | (NatDivisors m)) ) or n1 = n2 )
then A2: n1 = Sum ((EXP k) | (NatDivisors m)) ;
assume for m being natural non zero number st n = m holds
n2 = Sum ((EXP k) | (NatDivisors m)) ; :: thesis: n1 = n2
hence n1 = n2 by A2; :: thesis: verum

end;

( n <> 0 implies ex n1 being Element of NAT st
for m being natural non zero number 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 natural non zero number st n = m holds
n1 = Sum ((EXP k) | (NatDivisors m))
then reconsider n9 = n as natural non zero number ;
reconsider n1 = Sum ((EXP k) | (NatDivisors n9)) as Element of NAT by ORDINAL1:def 12;
take n1 ; :: thesis: for m being natural non zero number st n = m holds
n1 = Sum ((EXP k) | (NatDivisors m))
let m be natural non zero number ; :: thesis: ( n = m implies n1 = Sum ((EXP k) | (NatDivisors m)) )
assume n = m ; :: thesis: n1 = Sum ((EXP k) | (NatDivisors m))
hence 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 natural non zero number 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 natural non zero number st n = m holds
b₁ = Sum ((EXP k) | (NatDivisors m)) ) & ( for m being natural non zero number 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