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:15;
(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:15;
( 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 Th30;
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, Def3; :: thesis: verum