let S be non empty non void ManySortedSign ; :: thesis: for U1, U2, U3 being feasible MSAlgebra of 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 of 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 A1:
( 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 )
; :: thesis: ex GF being ManySortedFunction of U1,U3 st
( GF = G ** F & GF is_homomorphism U1,U3 )
then reconsider GF = G ** F as ManySortedFunction of U1,U3 by 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: verumproof
let o be
OperSymbol of
S;
:: according to MSUALG_3:def 9 :: thesis: ( Args o,U1 = {} or for b1 being Element of Args o,U1 holds (GF . (the_result_sort_of o)) . ((Den o,U1) . b1) = (Den o,U3) . (GF # b1) )
assume A2:
Args o,
U1 <> {}
;
:: thesis: for b1 being Element of Args o,U1 holds (GF . (the_result_sort_of o)) . ((Den o,U1) . b1) = (Den o,U3) . (GF # b1)
let x be
Element of
Args o,
U1;
:: thesis: (GF . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U3) . (GF # x)
set r =
the_result_sort_of o;
A3:
the
Sorts of
U1 is_transformable_to the
Sorts of
U3
by A1, AUTALG_1:11;
A4:
(F . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U2) . (F # x)
by A1, A2, MSUALG_3:def 9;
Args o,
U2 <> {}
by A1, A2, Th3;
then A5:
(G . (the_result_sort_of o)) . ((F . (the_result_sort_of o)) . ((Den o,U1) . x)) = (Den o,U3) . (G # (F # x))
by A1, A4, MSUALG_3:def 9;
A6:
GF . (the_result_sort_of o) = (G . (the_result_sort_of o)) * (F . (the_result_sort_of o))
by MSUALG_3:2;
A7:
dom (GF . (the_result_sort_of o)) = the
Sorts of
U1 . (the_result_sort_of o)
A8:
Result o,
U1 = (the Sorts of U1 * the ResultSort of S) . o
by MSUALG_1:def 10;
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 4;
then A9:
dom (the Sorts of U1 * the ResultSort of S) = dom the
ResultSort of
S
by RELAT_1:46;
o in the
carrier' of
S
;
then
o in dom the
ResultSort of
S
by FUNCT_2:def 1;
then A10:
Result o,
U1 =
the
Sorts of
U1 . (the ResultSort of S . o)
by A8, A9, FUNCT_1:22
.=
the
Sorts of
U1 . (the_result_sort_of o)
by MSUALG_1:def 7
;
then A11:
the
Sorts of
U1 . (the_result_sort_of o) <> {}
by A2, MSUALG_6:def 1;
consider gf being
ManySortedFunction of
U1,
U3 such that A12:
(
gf = G ** F &
gf # x = G # (F # x) )
by A1, A2, Th4;
thus
(GF . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U3) . (GF # x)
by A2, A5, A6, A7, A10, A11, A12, FUNCT_1:22, FUNCT_2:7;
:: thesis: verum
end;