( .: (G,A) is commutative & .: (G,A) is cancelable ) by Th24;
hence .: (G,A) is strict commutative constituted-Functions cancelable uniquely-decomposable Monoid by Th24; :: thesis: verum