let i, n be Element of NAT ; :: thesis: ( i is_expressible_by n implies ADD_MOD i,(NEG_MOD i,n),n = 0 )
assume i is_expressible_by n ; :: thesis: ADD_MOD i,(NEG_MOD i,n),n = 0
then i + (NEG_N i,n) = i + ((2 to_power n) - i) by Def5
.= 0 + (2 to_power n) ;
hence ADD_MOD i,(NEG_MOD i,n),n = (2 to_power n) mod (2 to_power n) by NAT_D:23
.= 0 by NAT_D:25 ;
:: thesis: verum