let U1 be Universal_Algebra; :: thesis: dom (signature U1) = dom the charact of U1
thus dom (signature U1) = Seg (len (signature U1)) by FINSEQ_1:def 3
.= Seg (len the charact of U1) by UNIALG_1:def 4
.= dom the charact of U1 by FINSEQ_1:def 3 ; :: thesis: verum