reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
set H = multLoopStr(# (UAEnd UA),(UAEndComp UA),i #);
thus UAEndMonoid UA is well-unital :: thesis: UAEndMonoid UA is associative
proof
let x be Element of (UAEndMonoid UA); :: according to VECTSP_1:def 6 :: 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;
for f, g, h being Element of multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) holds (f * g) * h = f * (g * h)
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 ;
A1: g * h = C * B by Def2;
f * g = B * A by Def2;
hence (f * g) * h = C * (B * A) by Def2
.= (C * B) * A by RELAT_1:36
.= f * (g * h) by A1, Def2 ;
:: thesis: verum
end;
then ( 1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = i & multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) is associative ) ;
hence UAEndMonoid UA is associative by Def3; :: thesis: verum