:: deftheorem Def5 defines OSSign OSALG_1:def 5 :
for S0 being non empty non void ManySortedSign
for b₂ being non empty non void strict order-sorted OverloadedRSSign holds
( b₂ = OSSign S0 iff ( the carrier of S0 = the carrier of b₂ & id the carrier of S0 = the InternalRel of b₂ & the carrier' of S0 = the carrier' of b₂ & id the carrier' of S0 = the Overloading of b₂ & the Arity of S0 = the Arity of b₂ & the ResultSort of S0 = the ResultSort of b₂ ) );