set s = OverloadedRSSign(# the carrier of S0,(id the carrier of S0), the carrier' of S0,(id the carrier' of S0), the Arity of S0, the ResultSort of S0 #);
reconsider s1 = OverloadedRSSign(# the carrier of S0,(id the carrier of S0), the carrier' of S0,(id the carrier' of S0), the Arity of S0, the ResultSort of S0 #) as non empty non void strict order-sorted OverloadedRSSign by Def1;
take s1 ; :: thesis: ( the carrier of S0 = the carrier of s1 & id the carrier of S0 = the InternalRel of s1 & the carrier' of S0 = the carrier' of s1 & id the carrier' of S0 = the Overloading of s1 & the Arity of S0 = the Arity of s1 & the ResultSort of S0 = the ResultSort of s1 )
thus ( the carrier of S0 = the carrier of s1 & id the carrier of S0 = the InternalRel of s1 & the carrier' of S0 = the carrier' of s1 & id the carrier' of S0 = the Overloading of s1 & the Arity of S0 = the Arity of s1 & the ResultSort of S0 = the ResultSort of s1 ) ; :: thesis: verum