reconsider i = id the carrier of UA as Element of UAEnd UA by Th3;
set M = multLoopStr(# (UAEnd UA),(UAEndComp UA),i #);
1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = i ;
hence not UAEndMonoid UA is empty by Def3; :: thesis: verum