set g9 = the carrier' of S -indexing g;
set gg = the carrier' of S -indexing g;
set f9 = the carrier of S -indexing f;
set ff = the carrier of S -indexing f;
A15: dom (the carrier' of S -indexing g) = the carrier' of S by PARTFUN1:def 4;
reconsider X = rng (the carrier of S -indexing f), Y = rng (the carrier' of S -indexing g) as non empty set ;
reconsider g9 = the carrier' of S -indexing g as Function of the carrier' of S,Y by A15, FUNCT_2:3;
consider G being rng-retract of g9;
A16: rng G c= the carrier' of S by A15, Th24;
dom G = rng g9 by Def2;
then reconsider G = G as Function of Y,the carrier' of S by A16, FUNCT_2:def 1, RELSET_1:11;
dom (the carrier of S -indexing f) = the carrier of S by PARTFUN1:def 4;
then reconsider f9 = the carrier of S -indexing f as Function of the carrier of S,X by FUNCT_2:3;
set r = (f9 * the ResultSort of S) * G;
take R = ManySortedSign(# X,Y,(((f9 * ) * the Arity of S) * G),((f9 * the ResultSort of S) * G) #); :: thesis: ( the carrier of S -indexing f,the carrier' of S -indexing g form_morphism_between S,R & the carrier of R = rng (the carrier of S -indexing f) & the carrier' of R = rng (the carrier' of S -indexing g) )
thus the carrier of S -indexing f,the carrier' of S -indexing g form_morphism_between S,R :: thesis: ( the carrier of R = rng (the carrier of S -indexing f) & the carrier' of R = rng (the carrier' of S -indexing g) )

proof

thus ( dom (the carrier of S -indexing f) = the carrier of S & dom (the carrier' of S -indexing g) = the carrier' of S ) by PARTFUN1:def 4; :: according to PUA2MSS1:def 13 :: thesis: ( proj2 (the carrier of S -indexing f) c= the carrier of R & proj2 (the carrier' of S -indexing g) c= the carrier' of R & the ResultSort of S * (the carrier of S -indexing f) = (the carrier' of S -indexing g) * the ResultSort of R & ( for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of S or not b₂ = the Arity of S . b₁ or b₂ * (the carrier of S -indexing f) = the Arity of R . ((the carrier' of S -indexing g) . b₁) ) ) )
thus ( rng (the carrier of S -indexing f) c= the carrier of R & rng (the carrier' of S -indexing g) c= the carrier' of R ) ; :: thesis: ( the ResultSort of S * (the carrier of S -indexing f) = (the carrier' of S -indexing g) * the ResultSort of R & ( for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of S or not b₂ = the Arity of S . b₁ or b₂ * (the carrier of S -indexing f) = the Arity of R . ((the carrier' of S -indexing g) . b₁) ) ) )

now

let x be OperSymbol of S; :: thesis: (((f9 * the ResultSort of S) * G) * g9) . x = (f9 * the ResultSort of S) . x
A17: g9 . (G . (g9 . x)) = g9 . x by Th25;
thus (((f9 * the ResultSort of S) * G) * g9) . x = the ResultSort of R . (g9 . x) by FUNCT_2:21
.= (f9 * the ResultSort of S) . (G . (g9 . x)) by FUNCT_2:21
.= f9 . (the_result_sort_of (G . (g9 . x))) by FUNCT_2:21
.= f9 . (the_result_sort_of x) by A1, A17, Th30
.= (f9 * the ResultSort of S) . x by FUNCT_2:21 ; :: thesis: verum

end;

hence (the carrier of S -indexing f) * the ResultSort of S = the ResultSort of R * (the carrier' of S -indexing g) by FUNCT_2:113; :: thesis: for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of S or not b₂ = the Arity of S . b₁ or b₂ * (the carrier of S -indexing f) = the Arity of R . ((the carrier' of S -indexing g) . b₁) )
let o be set ; :: thesis: for b₁ being set holds
( not o in the carrier' of S or not b₁ = the Arity of S . o or b₁ * (the carrier of S -indexing f) = the Arity of R . ((the carrier' of S -indexing g) . o) )
let p be Function; :: thesis: ( not o in the carrier' of S or not p = the Arity of S . o or p * (the carrier of S -indexing f) = the Arity of R . ((the carrier' of S -indexing g) . o) )
assume that
A18: o in the carrier' of S and
A19: p = the Arity of S . o ; :: thesis: p * (the carrier of S -indexing f) = the Arity of R . ((the carrier' of S -indexing g) . o)
reconsider x = o as OperSymbol of S by A18;
g9 . (G . (g9 . x)) = g9 . x by Th25;
then f9 * (the_arity_of x) = f9 * (the_arity_of (G . (g9 . x))) by A1, Th30;
hence (the carrier of S -indexing f) * p = (f9 * ) . (the_arity_of (G . (g9 . x))) by A19, LANG1:def 14
.= ((f9 * ) * the Arity of S) . (G . (g9 . x)) by FUNCT_2:21
.= the Arity of R . ((the carrier' of S -indexing g) . o) by FUNCT_2:21 ;
:: thesis: verum

end;

thus ( the carrier of R = rng (the carrier of S -indexing f) & the carrier' of R = rng (the carrier' of S -indexing g) ) ; :: thesis: verum