let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S holds Image (id the Sorts of A) = MSAlgebra(# the Sorts of A, the Charact of A #)
let A be non-empty MSAlgebra over S; :: thesis: Image (id the Sorts of A) = MSAlgebra(# the Sorts of A, the Charact of A #)
( MSAlgebra(# the Sorts of A, the Charact of A #) is strict non-empty MSSubAlgebra of A & id the Sorts of A is_homomorphism A,A & (id the Sorts of A) .:.: the Sorts of A = the Sorts of A ) by EQUATION:15, MSUALG_2:5, MSUALG_3:9;
hence Image (id the Sorts of A) = MSAlgebra(# the Sorts of A, the Charact of A #) by MSUALG_3:def 12; :: thesis: verum