let S be non void Signature; 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; ( 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
; ( 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; verum