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 that
A1: dom f c= the carrier of S and
A2: 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) )
A3: the carrier' of S -indexing g = (id the carrier' of S) +* g by A2, RELAT_1:68;
the carrier of S -indexing f = (id the carrier of S) +* f by A1, RELAT_1:68;
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 A3, Th40; :: thesis: verum