( the_unity_wrt addnat = 0 & ex n being Element of NAT st n is_a_unity_wrt addnat ) by Th40, Th43, SETWISEO:def 2;
hence 0 is_a_unity_wrt addnat by BINOP_1:def 8; :: thesis: addnat is uniquely-decomposable
thus addnat is uniquely-decomposable by Def20, Th43; :: thesis: verum