let U1, U2 be Universal_Algebra; :: thesis: ( U1,U2 are_similar implies len the charact of U1 = len the charact of U2 )
assume A1: U1,U2 are_similar ; :: thesis: len the charact of U1 = len the charact of U2
( len (signature U1) = len the charact of U1 & len (signature U2) = len the charact of U2 ) by UNIALG_1:def 11;
hence len the charact of U1 = len the charact of U2 by A1, Def2; :: thesis: verum