let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: x * y = g ** f

hence x * y = g ** f by A1, Def5; :: thesis: verum

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; :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: x * y = g ** f

hence x * y = g ** f by A1, Def5; :: thesis: verum