:: deftheorem defines form_a_replacement_in ALGSPEC1:def 3 :
for S being non empty non void ManySortedSign
for f, g being Function holds
( f,g form_a_replacement_in S iff for o1, o2 being OperSymbol of S st ((id the carrier' of S) +* g) . o1 = ((id the carrier' of S) +* g) . o2 holds
( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) ) );