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 Th52, Th54, BINOP_1:def 8; :: thesis: multnat is uniquely-decomposable
thus multnat is uniquely-decomposable by Def20, Th52; :: thesis: verum