reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
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