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 :: thesis: MSAEndMonoid U1 is associative

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

set H = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #);

thus MSAEndMonoid U1 is well-unital :: thesis: MSAEndMonoid U1 is associative

proof

for f, g, h being Element of multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) holds (f * g) * h = f * (g * h)
let x be Element of (MSAEndMonoid U1); :: according to VECTSP_1:def 6 :: 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;1. (MSAEndMonoid U1) = i by Def6;

hence ( x * (1. (MSAEndMonoid U1)) = x & (1. (MSAEndMonoid U1)) * x = x ) by Lm2; :: thesis: verum

proof

then
( 1. multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) = i & multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) is associative )
;
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 ;

A1: g * h = C ** B by Def5;

f * g = B ** A by Def5;

hence (f * g) * h = C ** (B ** A) by Def5

.= (C ** B) ** A by PBOOLE:140

.= f * (g * h) by A1, Def5 ;

:: thesis: verum

end;reconsider A = f, B = g, C = h as Element of MSAEnd U1 ;

A1: g * h = C ** B by Def5;

f * g = B ** A by Def5;

hence (f * g) * h = C ** (B ** A) by Def5

.= (C ** B) ** A by PBOOLE:140

.= f * (g * h) by A1, Def5 ;

:: thesis: verum

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