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 A1, ALTCAT_2:4;

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

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 A1, ALTCAT_2:4;

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 b_{1} being Element of Args (o,U1) holds (GF . (the_result_sort_of o)) . ((Den (o,U1)) . b_{1}) = (Den (o,U3)) . (GF # b_{1}) )

assume A5: Args (o,U1) <> {} ; :: thesis: for b_{1} being Element of Args (o,U1) holds (GF . (the_result_sort_of o)) . ((Den (o,U1)) . b_{1}) = (Den (o,U3)) . (GF # b_{1})

let x be Element of Args (o,U1); :: thesis: (GF . (the_result_sort_of o)) . ((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 . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) & Args (o,U2) <> {} ) by A1, A3, A5, Th3;

then A7: (G . (the_result_sort_of o)) . ((F . (the_result_sort_of o)) . ((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 A1, A2, AUTALG_1:10;

A9: dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o)

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 MSUALG_1:def 5, RELAT_1:27;

then A11: Result (o,U1) = the Sorts of U1 . ( the ResultSort of S . o) by A10, FUNCT_1:12

.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def 2 ;

then ( GF . (the_result_sort_of o) = (G . (the_result_sort_of o)) * (F . (the_result_sort_of o)) & the Sorts of U1 . (the_result_sort_of o) <> {} ) by A5, MSUALG_3:2, MSUALG_6:def 1;

hence (GF . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . (GF # x) by A5, A7, A9, A11, A6, FUNCT_1:12, FUNCT_2:5; :: thesis: verum

end;assume A5: Args (o,U1) <> {} ; :: thesis: for b

let x be Element of Args (o,U1); :: thesis: (GF . (the_result_sort_of o)) . ((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 . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) & Args (o,U2) <> {} ) by A1, A3, A5, Th3;

then A7: (G . (the_result_sort_of o)) . ((F . (the_result_sort_of o)) . ((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 A1, A2, AUTALG_1:10;

A9: dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o)

proof
end;

o in the carrier' of S
;per cases
( the Sorts of U1 . (the_result_sort_of o) <> {} or the Sorts of U1 . (the_result_sort_of o) = {} )
;

end;

suppose
the Sorts of U1 . (the_result_sort_of o) <> {}
; :: thesis: dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o)

then
the Sorts of U3 . (the_result_sort_of o) <> {}
by A8, PZFMISC1:def 3;

hence dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) by FUNCT_2:def 1; :: thesis: verum

end;hence dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) by FUNCT_2:def 1; :: thesis: verum

suppose
the Sorts of U1 . (the_result_sort_of o) = {}
; :: thesis: dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o)

hence
dom (GF . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o)
; :: thesis: verum

end;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 MSUALG_1:def 5, RELAT_1:27;

then A11: Result (o,U1) = the Sorts of U1 . ( the ResultSort of S . o) by A10, FUNCT_1:12

.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def 2 ;

then ( GF . (the_result_sort_of o) = (G . (the_result_sort_of o)) * (F . (the_result_sort_of o)) & the Sorts of U1 . (the_result_sort_of o) <> {} ) by A5, MSUALG_3:2, MSUALG_6:def 1;

hence (GF . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . (GF # x) by A5, A7, A9, A11, A6, FUNCT_1:12, FUNCT_2:5; :: thesis: verum