let S be non empty non void ManySortedSign ; :: thesis: 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 )
let f, g be Function; :: thesis: ( 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 )
(id the carrier' of S) +* (id the carrier' of S) = id the carrier' of S ;
then A1: (id the carrier' of S) +* ((id the carrier' of S) +* (g | the carrier' of S)) = (id the carrier' of S) +* (g | the carrier' of S) by FUNCT_4:14;
(id the carrier of S) +* (id the carrier of S) = id the carrier of S ;
then A2: (id the carrier of S) +* ((id the carrier of S) +* (f | the carrier of S)) = (id the carrier of S) +* (f | the carrier of S) by FUNCT_4:14;
( f,g form_a_replacement_in S iff for o1, o2 being OperSymbol of S st ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 holds
( ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) & ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2) ) ) by Th29;
hence ( 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 ) by A1, A2; :: thesis: verum