let S be non empty non void ManySortedSign ; 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; 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 7 ( 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;
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)
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 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;
verum
end;