let S be non empty non void ManySortedSign ; :: thesis: for U1, U2, U3 being feasible MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF is_homomorphism U1,U3 )

let U1, U2, U3 be feasible MSAlgebra over S; :: thesis: for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF is_homomorphism U1,U3 )

let F be ManySortedFunction of U1,U2; :: thesis: for G being ManySortedFunction of U2,U3 st the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 holds
ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF is_homomorphism U1,U3 )

let G be ManySortedFunction of U2,U3; :: thesis: ( the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism U1,U2 & G is_homomorphism U2,U3 implies ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF is_homomorphism U1,U3 ) )

assume that
A1: the Sorts of U1 is_transformable_to the Sorts of U2 and
A2: the Sorts of U2 is_transformable_to the Sorts of U3 and
A3: F is_homomorphism U1,U2 and
A4: G is_homomorphism U2,U3 ; :: thesis: ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF is_homomorphism U1,U3 )

reconsider GF = G ** F as ManySortedFunction of U1,U3 by ;
take GF ; :: thesis: ( GF = G ** F & GF is_homomorphism U1,U3 )
thus GF = G ** F ; :: thesis: GF is_homomorphism U1,U3
thus GF is_homomorphism U1,U3 :: thesis: verum
proof
let o be OperSymbol of S; :: according to MSUALG_3:def 7 :: thesis: ( Args (o,U1) = {} or for b1 being Element of Args (o,U1) holds (GF . ) . ((Den (o,U1)) . b1) = (Den (o,U3)) . (GF # b1) )
assume A5: Args (o,U1) <> {} ; :: thesis: for b1 being Element of Args (o,U1) holds (GF . ) . ((Den (o,U1)) . b1) = (Den (o,U3)) . (GF # b1)
let x be Element of Args (o,U1); :: thesis: (GF . ) . ((Den (o,U1)) . x) = (Den (o,U3)) . (GF # x)
A6: ex gf being ManySortedFunction of U1,U3 st
( gf = G ** F & gf # x = G # (F # x) ) by A1, A2, A5, Th4;
set r = the_result_sort_of o;
( (F . ) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) & Args (o,U2) <> {} ) by A1, A3, A5, Th3;
then A7: (G . ) . ((F . ) . ((Den (o,U1)) . x)) = (Den (o,U3)) . (G # (F # x)) by A4;
A8: the Sorts of U1 is_transformable_to the Sorts of U3 by ;
A9: dom (GF . ) = the Sorts of U1 .
proof
per cases ( the Sorts of U1 . <> {} or the Sorts of U1 . = {} ) ;
suppose the Sorts of U1 . <> {} ; :: thesis: dom (GF . ) = the Sorts of U1 .
then the Sorts of U3 . <> {} by ;
hence dom (GF . ) = the Sorts of U1 . by FUNCT_2:def 1; :: thesis: verum
end;
suppose the Sorts of U1 . = {} ; :: thesis: dom (GF . ) = the Sorts of U1 .
hence dom (GF . ) = the Sorts of U1 . ; :: thesis: verum
end;
end;
end;
o in the carrier' of S ;
then A10: o in dom the ResultSort of S by FUNCT_2:def 1;
rng the ResultSort of S c= the carrier of S ;
then rng the ResultSort of S c= dom the Sorts of U1 by PARTFUN1:def 2;
then ( Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o & dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S ) by ;
then A11: Result (o,U1) = the Sorts of U1 . ( the ResultSort of S . o) by
.= the Sorts of U1 . by MSUALG_1:def 2 ;
then ( GF . = (G . ) * (F . ) & the Sorts of U1 . <> {} ) by ;
hence (GF . ) . ((Den (o,U1)) . x) = (Den (o,U3)) . (GF # x) by ; :: thesis: verum
end;