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
proof
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;
for f, g, h being Element of multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) holds (f * g) * h = f * (g * h)
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 ;
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;
then ( 1. multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) = i & multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) is associative ) ;
hence MSAEndMonoid U1 is associative by Def6; :: thesis: verum