let U0, U1 be Universal_Algebra; :: thesis: ( U0 is SubAlgebra of U1 implies dom the charact of U0 = dom the charact of U1 )
assume A1: U0 is SubAlgebra of U1 ; :: thesis: dom the charact of U0 = dom the charact of U1
then reconsider A = the carrier of U0 as non empty Subset of U1 by Def7;
the charact of U0 = Opers (U1,A) by A1, Def7;
hence dom the charact of U0 = dom the charact of U1 by Def6; :: thesis: verum