( .: 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