let C1, C2 be Category; for F being Functor of C1,C2
for a, b, c being Object of C1
for f, g being Morphism of C1 st f in Hom (a,b) & g in Hom (b,c) holds
for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds
for 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)) holds
H # x = <*(F . g),(F . f)*>
let F be Functor of C1,C2; for a, b, c being Object of C1
for f, g being Morphism of C1 st f in Hom (a,b) & g in Hom (b,c) holds
for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds
for 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)) holds
H # x = <*(F . g),(F . f)*>
set CS1 = CatSign the carrier of C1;
set CS2 = CatSign the carrier of C2;
set A1 = MSAlg C1;
set A2 = MSAlg C2;
set u = Upsilon F;
set p = Psi F;
set B = (MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F));
let a, b, c be Object of C1; for f, g being Morphism of C1 st f in Hom (a,b) & g in Hom (b,c) holds
for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds
for 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)) holds
H # x = <*(F . g),(F . f)*>
set o = compsym (a,b,c);
let f, g be Morphism of C1; ( f in Hom (a,b) & g in Hom (b,c) implies for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds
for 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)) holds
H # x = <*(F . g),(F . f)*> )
assume that
A1:
f in Hom (a,b)
and
A2:
g in Hom (b,c)
; for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds
for 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)) holds
H # x = <*(F . g),(F . f)*>
let x be Element of Args ((compsym (a,b,c)),(MSAlg C1)); ( x = <*g,f*> implies for 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)) holds
H # x = <*(F . g),(F . f)*> )
assume A3:
x = <*g,f*>
; for 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)) holds
H # x = <*(F . g),(F . f)*>
F . g in Hom ((F . b),(F . c))
by A2, CAT_1:81;
then A4:
( dom (F . g) = F . b & cod (F . g) = F . c )
by CAT_1:1;
F . f in Hom ((F . a),(F . b))
by A1, CAT_1:81;
then
( dom (F . f) = F . a & cod (F . f) = F . b )
by CAT_1:1;
then A5:
<*(F . g),(F . f)*> in Args ((compsym ((F . a),(F . b),(F . c))),(MSAlg C2))
by A4, Th29;
A6:
( dom g = b & cod g = c )
by A2, CAT_1:1;
( dom f = a & cod f = b )
by A1, CAT_1:1;
then A7:
x in Args ((compsym (a,b,c)),(MSAlg C1))
by A3, A6, Th29;
let H be ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))); ( H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) implies H # x = <*(F . g),(F . f)*> )
assume A8:
H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1))
; H # x = <*(F . g),(F . f)*>
the Sorts of (MSAlg C1) . (homsym (b,c)) = Hom (b,c)
by Def13;
then
H . (homsym (b,c)) = F | (Hom (b,c))
by A8, Def1;
then A9:
(H . (homsym (b,c))) . g = F . g
by A2, FUNCT_1:49;
A10:
dom <*g,f*> = Seg 2
by FINSEQ_1:89;
then A11:
1 in dom <*g,f*>
by FINSEQ_1:2, TARSKI:def 2;
the Sorts of (MSAlg C1) . (homsym (a,b)) = Hom (a,b)
by Def13;
then
H . (homsym (a,b)) = F | (Hom (a,b))
by A8, Def1;
then A12:
(H . (homsym (a,b))) . f = F . f
by A1, FUNCT_1:49;
A13:
2 in dom <*g,f*>
by A10, FINSEQ_1:2, TARSKI:def 2;
Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2
by Th24;
then A14: Args ((compsym (a,b,c)),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)))) =
Args (((Psi F) . (compsym (a,b,c))),(MSAlg C2))
by INSTALG1:24
.=
Args ((compsym ((F . a),(F . b),(F . c))),(MSAlg C2))
by Th23
;
then consider g9, f9 being Morphism of C2 such that
A15:
H # x = <*g9,f9*>
and
dom f9 = F . a
and
cod f9 = F . b
and
dom g9 = F . b
and
cod g9 = F . c
by A5, Th29;
A16:
<*g9,f9*> . 1 = g9
by FINSEQ_1:44;
A17:
the_arity_of (compsym (a,b,c)) = <*(homsym (b,c)),(homsym (a,b))*>
by Def3;
then
( <*g,f*> . 1 = g & (the_arity_of (compsym (a,b,c))) /. 1 = homsym (b,c) )
by FINSEQ_1:44, FINSEQ_4:17;
then A18:
<*g9,f9*> . 1 = F . g
by A3, A7, A5, A14, A15, A9, A11, MSUALG_3:24;
( <*g,f*> . 2 = f & (the_arity_of (compsym (a,b,c))) /. 2 = homsym (a,b) )
by A17, FINSEQ_1:44, FINSEQ_4:17;
then
<*g9,f9*> . 2 = F . f
by A3, A7, A5, A14, A15, A12, A13, MSUALG_3:24;
hence
H # x = <*(F . g),(F . f)*>
by A15, A18, A16, FINSEQ_1:44; verum