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 ) )

for m being non zero Nat st n = m holds

n1 = Sum ((EXP k) | (NatDivisors m)) )_{1} being Element of NAT holds verum ) & ( n <> 0 implies ex b_{1} being Element of NAT st

for m being non zero Nat st n = m holds

b_{1} = Sum ((EXP k) | (NatDivisors m)) ) & ( not n <> 0 implies ex b_{1} being Element of NAT st b_{1} = 0 ) & ( for b_{1}, b_{2} being Element of NAT holds

( ( n <> 0 & ( for m being non zero Nat st n = m holds

b_{1} = Sum ((EXP k) | (NatDivisors m)) ) & ( for m being non zero Nat st n = m holds

b_{2} = Sum ((EXP k) | (NatDivisors m)) ) implies b_{1} = b_{2} ) & ( not n <> 0 & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) ) ) )
by A1; :: thesis: verum

( ( 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

( n <> 0 implies ex n1 being Element of NAT st
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;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

for m being non zero Nat st n = m holds

n1 = Sum ((EXP k) | (NatDivisors m)) )

proof

hence
( ( for b
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;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

for m being non zero Nat st n = m holds

b

( ( n <> 0 & ( for m being non zero Nat st n = m holds

b

b