let S be non empty non void ManySortedSign ; 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; 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; 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; ( 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
; 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
; ( GF = G ** F & GF is_homomorphism U1,U3 )
thus
GF = G ** F
; GF is_homomorphism U1,U3
thus
GF is_homomorphism U1,U3
verumproof
let o be
OperSymbol of
S;
MSUALG_3:def 9 ( 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 A5:
Args o,
U1 <> {}
;
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;
(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, MSUALG_3:def 9;
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, MSUALG_3:def 9;
A8:
the
Sorts of
U1 is_transformable_to the
Sorts of
U3
by A1, A2, AUTALG_1:11;
A9:
dom (GF . (the_result_sort_of o)) = the
Sorts of
U1 . (the_result_sort_of o)
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 4;
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 10, RELAT_1:46;
then A11:
Result o,
U1 =
the
Sorts of
U1 . (the ResultSort of S . o)
by A10, FUNCT_1:22
.=
the
Sorts of
U1 . (the_result_sort_of o)
by MSUALG_1:def 7
;
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:22, FUNCT_2:7;
verum
end;