let S be non void Signature; :: thesis: for f, g being Function st dom f c= the carrier of S & dom g c= the carrier' of S & f,g form_a_replacement_in S holds
(id the carrier of S) +* f,(id the carrier' of S) +* g form_morphism_between S,S with-replacement f,g
let f, g be Function; :: thesis: ( dom f c= the carrier of S & dom g c= the carrier' of S & f,g form_a_replacement_in S implies (id the carrier of S) +* f,(id the carrier' of S) +* g form_morphism_between S,S with-replacement f,g )
assume ( dom f c= the carrier of S & dom g c= the carrier' of S ) ; :: thesis: ( not f,g form_a_replacement_in S or (id the carrier of S) +* f,(id the carrier' of S) +* g form_morphism_between S,S with-replacement f,g )
then ( the carrier of S -indexing f = (id the carrier of S) +* f & the carrier' of S -indexing g = (id the carrier' of S) +* g ) by RELAT_1:97;
hence ( not f,g form_a_replacement_in S or (id the carrier of S) +* f,(id the carrier' of S) +* g form_morphism_between S,S with-replacement f,g ) by Th41; :: thesis: verum