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:123;
then A4: ( dom (F . g) = F . b & cod (F . g) = F . c ) by CAT_1:18;
F . f in Hom (F . a),(F . b) by A1, CAT_1:123;
then ( dom (F . f) = F . a & cod (F . f) = F . b ) by CAT_1:18;
then A5: <*(F . g),(F . f)*> in Args (compsym (F . a),(F . b),(F . c)),(MSAlg C2) by A4, Th39;
A6: ( dom g = b & cod g = c ) by A2, CAT_1:18;
( dom f = a & cod f = b ) by A1, CAT_1:18;
then A7: x in Args (compsym a,b,c),(MSAlg C1) by A3, A6, Th39;
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 Def15;
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:72;
A10: dom <*g,f*> = Seg 2 by FINSEQ_3:29;
then A11: 1 in dom <*g,f*> by FINSEQ_1:4, TARSKI:def 2;
the Sorts of (MSAlg C1) . (homsym a,b) = Hom a,b by Def15;
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:72;
A13: 2 in dom <*g,f*> by A10, FINSEQ_1:4, TARSKI:def 2;
Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2 by Th33;
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:25
.= Args (compsym (F . a),(F . b),(F . c)),(MSAlg C2) by Th32 ;
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, Th39;
A16: <*g9,f9*> . 1 = g9 by FINSEQ_1:61;
A17: the_arity_of (compsym a,b,c) = <*(homsym b,c),(homsym a,b)*> by Def5;
then ( <*g,f*> . 1 = g & (the_arity_of (compsym a,b,c)) /. 1 = homsym b,c ) by FINSEQ_1:61, FINSEQ_4:26;
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:61, FINSEQ_4:26;
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:61; :: thesis: verum