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

A2: ( not n <> 0 implies ex n1 being Element of NAT st n1 = 0 )

proof

assume not n <> 0 ; :: thesis: ex n1 being Element of NAT st n1 = 0
reconsider n1 = 0 as Element of NAT by ORDINAL1:def 13;
take n1 ; :: thesis: n1 = 0
thus n1 = 0 ; :: thesis: verum

end;

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