let C1, C2 be Category; for F being Functor of C1,C2 ex H being ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) st
( H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) & H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)) )
let F be Functor of C1,C2; ex H being ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) st
( H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) & H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)) )
set S1 = CatSign the carrier of C1;
set S2 = CatSign the carrier of C2;
set A1 = MSAlg C1;
set A2 = MSAlg C2;
set f = Upsilon F;
set G = Psi F;
set B1 = (MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F));
A1:
Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2
by Th33;
reconsider H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) as ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) by Th38;
take
H
; ( H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) & H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)) )
thus
H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1))
; H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))
let o be OperSymbol of (CatSign the carrier of C1); MSUALG_3:def 9 ( Args (o,(MSAlg C1)) = {} or for b1 being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b1) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b1) )
assume A2:
Args (o,(MSAlg C1)) <> {}
; for b1 being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b1) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b1)
per cases
( o `1 = 1 or o `1 = 2 )
by Th25;
suppose
o `1 = 1
;
for b1 being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b1) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b1)then consider a being
Object of
C1 such that A3:
o = idsym a
by Th26;
let x be
Element of
Args (
o,
(MSAlg C1));
(H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . x) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x)A4:
Args (
((Psi F) . o),
(MSAlg C2))
= Args (
o,
((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))
by A1, INSTALG1:25;
A5:
(Psi F) . o = idsym (F . a)
by A3, Th31;
then
Args (
((Psi F) . o),
(MSAlg C2))
= {{}}
by Th34;
then A6:
H # x = {}
by A4, TARSKI:def 1;
reconsider h =
id a as
Morphism of
a,
a ;
(
dom (id a) = a &
cod (id a) = a )
by CAT_1:44;
then A7:
id a in Hom (
a,
a)
by CAT_1:18;
Args (
o,
(MSAlg C1))
= {{}}
by A3, Th34;
then
x = {}
by TARSKI:def 1;
hence (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . x) =
(H . (the_result_sort_of o)) . h
by A3, Def15
.=
(H . (homsym (a,a))) . h
by A3, Def5
.=
(F | ( the Sorts of (MSAlg C1) . (homsym (a,a)))) . h
by Def1
.=
(F | (Hom (a,a))) . h
by Def15
.=
(hom (F,a,a)) . h
by CAT_1:def 25
.=
F . h
by A7, CAT_1:131
.=
id (F . a)
by CAT_1:108
.=
(Den (((Psi F) . o),(MSAlg C2))) . (H # x)
by A5, A6, Def15
.=
(Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x)
by Th33, INSTALG1:24
;
verum end; suppose A8:
o `1 = 2
;
for b1 being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b1) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b1)let x be
Element of
Args (
o,
(MSAlg C1));
(H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . x) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x)consider a,
b,
c being
Object of
C1 such that A9:
o = compsym (
a,
b,
c)
by A8, Th27;
A10:
(Psi F) . o = compsym (
(F . a),
(F . b),
(F . c))
by A9, Th32;
consider g,
h being
Morphism of
C1 such that A11:
x = <*g,h*>
and A12:
dom h = a
and A13:
cod h = b
and A14:
dom g = b
and A15:
cod g = c
by A2, A9, Th39;
A16:
(
g in Hom (
b,
c) &
h in Hom (
a,
b) )
by A12, A13, A14, A15, CAT_1:18;
(
dom (g * h) = a &
cod (g * h) = c )
by A12, A13, A14, A15, CAT_1:42;
then A17:
g * h in Hom (
a,
c)
by CAT_1:18;
then reconsider gh =
g * h as
Morphism of
a,
c by CAT_1:def 7;
A18:
(
dom (F . h) = F . a &
cod (F . h) = F . b )
by A12, A13, CAT_1:109;
A19:
(
dom (F . g) = F . b &
cod (F . g) = F . c )
by A14, A15, CAT_1:109;
thus (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . x) =
(H . (the_result_sort_of o)) . gh
by A9, A11, A12, A13, A14, A15, Def15
.=
(H . (homsym (a,c))) . gh
by A9, Def5
.=
(F | ( the Sorts of (MSAlg C1) . (homsym (a,c)))) . gh
by Def1
.=
(F | (Hom (a,c))) . gh
by Def15
.=
(hom (F,a,c)) . gh
by CAT_1:def 25
.=
F . gh
by A17, CAT_1:131
.=
(F . g) * (F . h)
by A13, A14, CAT_1:99
.=
(Den (((Psi F) . o),(MSAlg C2))) . <*(F . g),(F . h)*>
by A10, A18, A19, Def15
.=
(Den (((Psi F) . o),(MSAlg C2))) . (H # x)
by A9, A11, A16, Th40
.=
(Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x)
by Th33, INSTALG1:24
;
verum end;