set A = the Universal_Algebra;
reconsider f = (*--> 0) * (signature the Universal_Algebra) as Function of (dom (signature the Universal_Algebra)),({0} *) by Th2;
( ManySortedSign(# {0},(dom (signature the Universal_Algebra)),f,((dom (signature the Universal_Algebra)) --> z) #) is segmental & not ManySortedSign(# {0},(dom (signature the Universal_Algebra)),f,((dom (signature the Universal_Algebra)) --> z) #) is void & ManySortedSign(# {0},(dom (signature the Universal_Algebra)),f,((dom (signature the Universal_Algebra)) --> z) #) is strict & ManySortedSign(# {0},(dom (signature the Universal_Algebra)),f,((dom (signature the Universal_Algebra)) --> z) #) is 1 -element ) by Lm2;
hence ex b₁ being ManySortedSign st
( b₁ is segmental & not b₁ is void & b₁ is strict & b₁ is 1 -element ) ; :: thesis: verum