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