let S be non void Signature; :: thesis: for f, g being Function st f,g form_a_replacement_in S holds
for f' being Function of the carrier of S,the carrier of (S with-replacement f,g) st f' = the carrier of S -indexing f holds
for g' being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement f,g) = ((f' * ) * the Arity of S) * g'
let f, g be Function; :: thesis: ( f,g form_a_replacement_in S implies for f' being Function of the carrier of S,the carrier of (S with-replacement f,g) st f' = the carrier of S -indexing f holds
for g' being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement f,g) = ((f' * ) * the Arity of S) * g' )
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 f' being Function of the carrier of S,the carrier of (S with-replacement f,g) st f' = the carrier of S -indexing f holds
for g' being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement f,g) = ((f' * ) * the Arity of S) * g'
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 f' be Function of the carrier of S,the carrier of (S with-replacement f,g); :: thesis: ( f' = the carrier of S -indexing f implies for g' being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement f,g) = ((f' * ) * the Arity of S) * g' )
assume A3: f' = the carrier of S -indexing f ; :: thesis: for g' being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement f,g) = ((f' * ) * the Arity of S) * g'
let g' be rng-retract of the carrier' of S -indexing g; :: thesis: the Arity of (S with-replacement f,g) = ((f' * ) * the Arity of S) * g'
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:23
.= the Arity of (S with-replacement f,g) * ((the carrier' of S -indexing g) * g') by Def2
.= (the Arity of (S with-replacement f,g) * (the carrier' of S -indexing g)) * g' by RELAT_1:55
.= ((f' * ) * the Arity of S) * g' by A2, A3, Th36 ;
:: thesis: verum