let C1, C2 be Category; :: thesis: 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; :: thesis: 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
; :: thesis: ( 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)
; :: thesis: 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); :: according to MSUALG_3:def 9 :: thesis: ( 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) <> {}
; :: thesis: 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
;
:: thesis: 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;
A4:
(Psi F) . o = idsym (F . a)
by A3, Th31;
let x be
Element of
Args o,
(MSAlg C1);
:: thesis: (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)
(
x in Args o,
(MSAlg C1) &
Args o,
(MSAlg C1) = {{} } &
Args ((Psi F) . o),
(MSAlg C2) = {{} } &
Args ((Psi F) . o),
(MSAlg C2) = Args o,
((MSAlg C2) | (CatSign the carrier of C1),(Upsilon F),(Psi F)) )
by A1, A2, A3, A4, Th34, INSTALG1:25;
then A5:
(
x = {} &
H # x = {} &
dom (id a) = a &
cod (id a) = a )
by CAT_1:44, TARSKI:def 1;
then A6:
id a in Hom a,
a
by CAT_1:18;
reconsider h =
id a as
Morphism of
a,
a ;
thus (H . (the_result_sort_of o)) . ((Den o,(MSAlg C1)) . x) =
(H . (the_result_sort_of o)) . h
by A3, A5, 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 A6, CAT_1:131
.=
id (F . a)
by CAT_1:108
.=
(Den ((Psi F) . o),(MSAlg C2)) . (H # x)
by A4, A5, Def15
.=
(Den o,((MSAlg C2) | (CatSign the carrier of C1),(Upsilon F),(Psi F))) . (H # x)
by Th33, INSTALG1:24
;
:: thesis: verum end; suppose
o `1 = 2
;
:: thesis: 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,
b,
c being
Object of
C1 such that A7:
o = compsym a,
b,
c
by Th27;
A8:
(Psi F) . o = compsym (F . a),
(F . b),
(F . c)
by A7, Th32;
let x be
Element of
Args o,
(MSAlg C1);
:: thesis: (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 g,
h being
Morphism of
C1 such that A9:
(
x = <*g,h*> &
dom h = a &
cod h = b &
dom g = b &
cod g = c )
by A2, A7, Th39;
(
dom (g * h) = a &
cod (g * h) = c )
by A9, CAT_1:42;
then A10:
(
g * h in Hom a,
c &
g in Hom b,
c &
h in Hom a,
b )
by A9, CAT_1:18;
then reconsider gh =
g * h as
Morphism of
a,
c by CAT_1:def 7;
A11:
(
dom (F . h) = F . a &
cod (F . h) = F . b &
dom (F . g) = F . b &
cod (F . g) = F . c )
by A9, CAT_1:109;
thus (H . (the_result_sort_of o)) . ((Den o,(MSAlg C1)) . x) =
(H . (the_result_sort_of o)) . gh
by A7, A9, Def15
.=
(H . (homsym a,c)) . gh
by A7, 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 A10, CAT_1:131
.=
(F . g) * (F . h)
by A9, CAT_1:99
.=
(Den ((Psi F) . o),(MSAlg C2)) . <*(F . g),(F . h)*>
by A8, A11, Def15
.=
(Den ((Psi F) . o),(MSAlg C2)) . (H # x)
by A7, A9, A10, Th40
.=
(Den o,((MSAlg C2) | (CatSign the carrier of C1),(Upsilon F),(Psi F))) . (H # x)
by Th33, INSTALG1:24
;
:: thesis: verum end;