let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra over S holds id the Sorts of A is Endomorphism of A
let A be MSAlgebra over S; :: thesis: id the Sorts of A is Endomorphism of A
thus id the Sorts of A is_homomorphism A,A by MSUALG_3:9; :: according to MSUALG_6:def 2 :: thesis: verum