reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
set H = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #);
thus
MSAEndMonoid U1 is well-unital
MSAEndMonoid U1 is associative
for f, g, h being Element of multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) holds (f * g) * h = f * (g * h)
then
( 1. multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) = i & multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) is associative )
;
hence
MSAEndMonoid U1 is associative
by Def6; verum