let S be non void Signature; :: thesis: for f, g being Function st f,g form_a_replacement_in S holds
for f9 being Function of the carrier of S, the carrier of (S with-replacement (f,g)) st f9 = the carrier of S -indexing f holds
for g9 being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement (f,g)) = ((f9 *) * the Arity of S) * g9
let f, g be Function; :: thesis: ( f,g form_a_replacement_in S implies for f9 being Function of the carrier of S, the carrier of (S with-replacement (f,g)) st f9 = the carrier of S -indexing f holds
for g9 being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement (f,g)) = ((f9 *) * the Arity of S) * g9 )
set ff = the carrier of S -indexing f;
set gg = the carrier' of S -indexing g;
set T = S with-replacement (f,g);
assume A1: f,g form_a_replacement_in S ; :: thesis: for f9 being Function of the carrier of S, the carrier of (S with-replacement (f,g)) st f9 = the carrier of S -indexing f holds
for g9 being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement (f,g)) = ((f9 *) * the Arity of S) * g9
then A2: the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) by Def4;
let f9 be Function of the carrier of S, the carrier of (S with-replacement (f,g)); :: thesis: ( f9 = the carrier of S -indexing f implies for g9 being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement (f,g)) = ((f9 *) * the Arity of S) * g9 )
assume A3: f9 = the carrier of S -indexing f ; :: thesis: for g9 being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement (f,g)) = ((f9 *) * the Arity of S) * g9
let g9 be rng-retract of the carrier' of S -indexing g; :: thesis: the Arity of (S with-replacement (f,g)) = ((f9 *) * the Arity of S) * g9
the carrier' of (S with-replacement (f,g)) = rng ( the carrier' of S -indexing g) by A1, Def4;
hence the Arity of (S with-replacement (f,g)) = the Arity of (S with-replacement (f,g)) * (id (rng ( the carrier' of S -indexing g))) by FUNCT_2:17
.= the Arity of (S with-replacement (f,g)) * (( the carrier' of S -indexing g) * g9) by Def2
.= ( the Arity of (S with-replacement (f,g)) * ( the carrier' of S -indexing g)) * g9 by RELAT_1:36
.= ((f9 *) * the Arity of S) * g9 by A2, A3, Th35 ;
:: thesis: verum