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 that
A1: dom f = the carrier of S and
A2: 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) )
dom g = dom (id the carrier' of S) by A2;
then A3: (id the carrier' of S) +* g = g by FUNCT_4:19;
dom f = dom (id the carrier of S) by A1;
then (id the carrier of S) +* f = f by FUNCT_4:19;
hence ( not f,g form_a_replacement_in S or f,g form_morphism_between S,S with-replacement (f,g) ) by A1, A2, A3, Th41; :: thesis: verum