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