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

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