let C1, C2 be Category; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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)); :: thesis: ( 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*> ; :: thesis: 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))); :: thesis: ( 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)) ; :: thesis: 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;
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_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_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; :: thesis: verum