ex n being Element of NAT st n is_a_unity_wrt multnat by SETWISEO:def 2;
hence 1 is_a_unity_wrt multnat by Th61, Th63, BINOP_1:def 8; :: thesis: multnat is uniquely-decomposable
thus multnat is uniquely-decomposable by Def20, Th61; :: thesis: verum