reconsider s = the carrier of S --> {0} as ManySortedSet of the carrier of S ;
set o = the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S;
take
MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #)
; ( MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) is strict & MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) is non-empty )
thus
MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) is strict
; MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) is non-empty
let i be object ; PBOOLE:def 13,MSUALG_1:def 3 ( not i in the carrier of S or not the Sorts of MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) . i is empty )
assume
i in the carrier of S
; not the Sorts of MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) . i is empty
hence
not the Sorts of MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) . i is empty
; verum