let UA be Universal_Algebra; :: thesis: for x, y being Element of (UAEndMonoid UA)
for f, g being Element of UAEnd UA st x = f & y = g holds
x * y = g * f
reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
let x, y be Element of (UAEndMonoid UA); :: thesis: for f, g being Element of UAEnd UA st x = f & y = g holds
x * y = g * f
let f, g be Element of UAEnd UA; :: thesis: ( x = f & y = g implies x * y = g * f )
set H = multLoopStr(# (UAEnd UA),(UAEndComp UA),i #);
1. multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) = i ;
then A1: UAEndMonoid UA = multLoopStr(# (UAEnd UA),(UAEndComp UA),i #) by Def3;
assume ( x = f & y = g ) ; :: thesis: x * y = g * f
hence x * y = g * f by A1, Def2; :: thesis: verum