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 A1: ( f in Hom a,b & 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 A2: 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)*>
( dom f = a & cod f = b & dom g = b & cod g = c ) by A1, CAT_1:18;
then A3: x in Args (compsym a,b,c),(MSAlg C1) by A2, Th39;
A4: ( <*g,f*> . 1 = g & <*g,f*> . 2 = f ) by FINSEQ_1:61;
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 A5: H = F -MSF the carrier of (CatSign the carrier of C1),the Sorts of (MSAlg C1) ; :: thesis: H # x = <*(F . g),(F . f)*>
( F . f in Hom (F . a),(F . b) & F . g in Hom (F . b),(F . c) ) by A1, CAT_1:123;
then ( dom (F . f) = F . a & cod (F . f) = F . b & dom (F . g) = F . b & cod (F . g) = F . c ) by CAT_1:18;
then A6: <*(F . g),(F . f)*> in Args (compsym (F . a),(F . b),(F . c)),(MSAlg C2) by Th39;
Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2 by Th33;
then A7: 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 g', f' being Morphism of C2 such that
A8: ( H # x = <*g',f'*> & dom f' = F . a & cod f' = F . b & dom g' = F . b & cod g' = F . c ) by A6, Th39;
dom <*(homsym b,c),(homsym a,b)*> = Seg 2 by FINSEQ_3:29;
then ( 1 in dom <*(homsym b,c),(homsym a,b)*> & 2 in dom <*(homsym b,c),(homsym a,b)*> & the_arity_of (compsym a,b,c) = <*(homsym b,c),(homsym a,b)*> ) by Def5, FINSEQ_1:4, TARSKI:def 2;
then A9: ( (the_arity_of (compsym a,b,c)) /. 1 = homsym b,c & (the_arity_of (compsym a,b,c)) /. 2 = homsym a,b ) by FINSEQ_4:26;
( the Sorts of (MSAlg C1) . (homsym a,b) = Hom a,b & the Sorts of (MSAlg C1) . (homsym b,c) = Hom b,c ) by Def15;
then ( H . (homsym a,b) = F | (Hom a,b) & H . (homsym b,c) = F | (Hom b,c) ) by A5, Def1;
then A10: ( (H . (homsym a,b)) . f = F . f & (H . (homsym b,c)) . g = F . g ) by A1, FUNCT_1:72;
dom <*g,f*> = Seg 2 by FINSEQ_3:29;
then ( 1 in dom <*g,f*> & 2 in dom <*g,f*> ) by FINSEQ_1:4, TARSKI:def 2;
then ( <*g',f'*> . 2 = F . f & <*g',f'*> . 1 = F . g & <*g',f'*> . 1 = g' & <*g',f'*> . 2 = f' ) by A2, A3, A4, A6, A7, A8, A9, A10, FINSEQ_1:61, MSUALG_3:24;
hence H # x = <*(F . g),(F . f)*> by A8; :: thesis: verum