let S be non empty non void ManySortedSign ; :: thesis: for U1 being non-empty MSAlgebra over S
for f1, f2 being Element of MSAEnd U1 holds f1 ** f2 in MSAEnd U1
let U1 be non-empty MSAlgebra over S; :: thesis: for f1, f2 being Element of MSAEnd U1 holds f1 ** f2 in MSAEnd U1
let f1, f2 be Element of MSAEnd U1; :: thesis: f1 ** f2 in MSAEnd U1
( f1 is_homomorphism U1,U1 & f2 is_homomorphism U1,U1 ) by Def4;
then f1 ** f2 is_homomorphism U1,U1 by MSUALG_3:10;
hence f1 ** f2 in MSAEnd U1 by Def4; :: thesis: verum