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