reconsider f = (*--> 0) * (signature A) as Function of (dom (signature A)),({0} *) by Th2;
( 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 ) by Lm2;
hence ( ex b₁ being trivial non void strict segmental ManySortedSign st
( the carrier of b₁ = {0} & the carrier' of b₁ = dom (signature A) & the Arity of b₁ = (*--> 0) * (signature A) & the ResultSort of b₁ = (dom (signature A)) --> 0 ) & ( for b₁, b₂ being trivial non void strict segmental ManySortedSign st the carrier of b₁ = {0} & the carrier' of b₁ = dom (signature A) & the Arity of b₁ = (*--> 0) * (signature A) & the ResultSort of b₁ = (dom (signature A)) --> 0 & the carrier of b₂ = {0} & the carrier' of b₂ = dom (signature A) & the Arity of b₂ = (*--> 0) * (signature A) & the ResultSort of b₂ = (dom (signature A)) --> 0 holds
b₁ = b₂ ) ) ; :: thesis: verum