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

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