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 2;
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:1;
set G = the rng-retract of g9;
A16: rng the rng-retract of g9 c= the carrier' of S by A15, Th23;
dom the rng-retract of g9 = rng g9 by Def2;
then reconsider G = the rng-retract of g9 as Function of Y, the carrier' of S by A16, FUNCT_2:def 1, RELSET_1:4;
dom ( the carrier of S -indexing f) = the carrier of S by PARTFUN1:def 2;
then reconsider f9 = the carrier of S -indexing f as Function of the carrier of S,X by FUNCT_2:1;
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 2; :: according to PUA2MSS1:def 12 :: thesis: ( rng ( the carrier of S -indexing f) c= the carrier of R & rng ( 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 b1 being set
for b2 being set holds
( not b1 in the carrier' of S or not b2 = the Arity of S . b1 or b2 * ( the carrier of S -indexing f) = the Arity of R . (( the carrier' of S -indexing g) . b1) ) ) )
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 b1 being set
for b2 being set holds
( not b1 in the carrier' of S or not b2 = the Arity of S . b1 or b2 * ( the carrier of S -indexing f) = the Arity of R . (( the carrier' of S -indexing g) . b1) ) ) )
now :: thesis: for x being OperSymbol of S holds (((f9 * the ResultSort of S) * G) * g9) . x = (f9 * the ResultSort of S) . x
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 Th24;
thus (((f9 * the ResultSort of S) * G) * g9) . x = the ResultSort of R . (g9 . x) by FUNCT_2:15
.= (f9 * the ResultSort of S) . (G . (g9 . x)) by FUNCT_2:15
.= f9 . (the_result_sort_of (G . (g9 . x))) by FUNCT_2:15
.= f9 . (the_result_sort_of x) by A1, A17, Th29
.= (f9 * the ResultSort of S) . x by FUNCT_2:15 ; :: 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:63; :: thesis: for b1 being set
for b2 being set holds
( not b1 in the carrier' of S or not b2 = the Arity of S . b1 or b2 * ( the carrier of S -indexing f) = the Arity of R . (( the carrier' of S -indexing g) . b1) )
let o be set ; :: thesis: for b1 being set holds
( not o in the carrier' of S or not b1 = the Arity of S . o or b1 * ( 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 Th24;
then f9 * (the_arity_of x) = f9 * (the_arity_of (G . (g9 . x))) by A1, Th29;
hence ( the carrier of S -indexing f) * p = (f9 *) . (the_arity_of (G . (g9 . x))) by A19, LANG1:def 13
.= ((f9 *) * the Arity of S) . (G . (g9 . x)) by FUNCT_2:15
.= the Arity of R . (( the carrier' of S -indexing g) . o) by FUNCT_2:15 ;
:: 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