reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th10;
set H = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #);
thus MSAEndMonoid U1 is well-unital :: thesis: MSAEndMonoid U1 is associative

proof

let x be Element of (MSAEndMonoid U1); :: according to VECTSP_1:def 16 :: thesis: ( x * (1. (MSAEndMonoid U1)) = x & (1. (MSAEndMonoid U1)) * x = x )
1. (MSAEndMonoid U1) = i by Def6;
hence ( x * (1. (MSAEndMonoid U1)) = x & (1. (MSAEndMonoid U1)) * x = x ) by Lm2; :: thesis: verum

end;

A1: 1. multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) = i ;
multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) is associative

proof

thus for f, g, h being Element of multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) holds (f * g) * h = f * (g * h) :: according to GROUP_1:def 4 :: thesis: verum

proof

let f, g, h be Element of multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #); :: thesis: (f * g) * h = f * (g * h)
reconsider A = f, B = g, C = h as Element of MSAEnd U1 ;
A2: f * g = B ** A by Def5;
A3: g * h = C ** B by Def5;
thus (f * g) * h = C ** (B ** A) by A2, Def5
.= (C ** B) ** A by PBOOLE:154
.= f * (g * h) by A3, Def5 ; :: thesis: verum

end;

end;

hence MSAEndMonoid U1 is associative by A1, Def6; :: thesis: verum