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 #) ; :: thesis: ( 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 ; :: thesis: MSAlgebra(# s, the ManySortedFunction of (s #) * the Arity of S,s * the ResultSort of S #) is non-empty
let i be object ; :: according to PBOOLE:def 13,MSUALG_1:def 3 :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum