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 ) 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