consider A being Universal_Algebra;
reconsider f = (*--> 0 ) * (signature A) as Function of (dom (signature A)),({0 } * ) by Th7;
( ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is trivial & not ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is void & ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is strict & not ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> 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