reconsider i = id the carrier of UA as Element of UAEnd UA by Th3;
set H = multLoopStr(# (UAEnd UA),(UAEndComp UA),i #);
set F = UAEndMonoid UA;
thus UAEndMonoid UA is well-unital :: thesis: UAEndMonoid UA is associative

proof

let x be Element of (UAEndMonoid UA); :: according to VECTSP_1:def 16 :: thesis: ( x * (1. (UAEndMonoid UA)) = x & (1. (UAEndMonoid UA)) * x = x )
1. (UAEndMonoid UA) = i by Def3;
hence ( x * (1. (UAEndMonoid UA)) = x & (1. (UAEndMonoid UA)) * x = x ) by Lm1; :: thesis: verum

end;

A1: 1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = i ;
multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) is associative

proof

thus for f, g, h being Element of multLoopStr(# (UAEnd UA),(UAEndComp UA),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(# (UAEnd UA),(UAEndComp UA),i #); :: thesis: (f * g) * h = f * (g * h)
reconsider A = f, B = g, C = h as Element of UAEnd UA ;
A2: f * g = B * A by Def2;
A3: g * h = C * B by Def2;
thus (f * g) * h = C * (B * A) by A2, Def2
.= (C * B) * A by RELAT_1:55
.= f * (g * h) by A3, Def2 ; :: thesis: verum

end;

end;

hence UAEndMonoid UA is associative by A1, Def3; :: thesis: verum