for S being non empty non void ManySortedSign
for f, g being Function holds
( f,g form_a_replacement_in S iff the carrier of S -indexing f, the carrier' of S -indexing g form_a_replacement_in S )