let S be non empty non void ManySortedSign ; for U1 being non-empty MSAlgebra over S
for x, y being Element of (MSAEndMonoid U1)
for f, g being Element of MSAEnd U1 st x = f & y = g holds
x * y = g ** f
let U1 be non-empty MSAlgebra over S; for x, y being Element of (MSAEndMonoid U1)
for f, g being Element of MSAEnd U1 st x = f & y = g holds
x * y = g ** f
reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
let x, y be Element of (MSAEndMonoid U1); for f, g being Element of MSAEnd U1 st x = f & y = g holds
x * y = g ** f
let f, g be Element of MSAEnd U1; ( x = f & y = g implies x * y = g ** f )
set H = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #);
1. multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #) = i
;
then A1:
MSAEndMonoid U1 = multLoopStr(# (MSAEnd U1),(MSAEndComp U1),i #)
by Def6;
assume
( x = f & y = g )
; x * y = g ** f
hence
x * y = g ** f
by A1, Def5; verum