set A = the Universal_Algebra;
reconsider f = (*--> 0) * (signature the Universal_Algebra) as Function of (dom (signature the Universal_Algebra)),({0} *) by Th7;
( ManySortedSign(# {0},(dom (signature the Universal_Algebra)),f,((dom (signature the Universal_Algebra)) --> z) #) is segmental & ManySortedSign(# {0},(dom (signature the Universal_Algebra)),f,((dom (signature the Universal_Algebra)) --> z) #) is trivial & 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 & not ManySortedSign(# {0},(dom (signature the Universal_Algebra)),f,((dom (signature the Universal_Algebra)) --> z) #) is empty ) by Lm2;
hence ex b₁ being ManySortedSign st
( b₁ is segmental & b₁ is trivial & not b₁ is void & b₁ is strict & not b₁ is empty ) ; :: thesis: verum