reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
set H = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #);
1. multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) = i ;
hence not MSAEndMonoid U1 is empty by Def6; :: thesis: verum