let A be Universal_Algebra; :: thesis: not signature A is empty
len the charact of A <> 0 ;
then len (signature A) <> 0 by UNIALG_1:def 4;
hence not signature A is empty ; :: thesis: verum