let C1, C2 be Category; :: thesis:
let F be Functor of C1,C2; :: thesis:
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:
thus H = F -MSF the carrier of (CatSign the carrier of C1),the Sorts of (MSAlg C1) ; :: thesis:
let o be OperSymbol of (CatSign the carrier of C1); :: according to MSUALG_3:def 9 :: thesis:
assume A2: Args o,(MSAlg C1) <> {} ; :: thesis:

per cases by Th25;

suppose o `1 = 1 ; :: thesis:

then consider a being Object of C1 such that
A3: o = idsym a by Th26;
let x be Element of Args o,(MSAlg C1); :: thesis:
A4: Args ((Psi F) . o),(MSAlg C2) = Args o,((MSAlg C2) | (CatSign the carrier of C1),(Upsilon F),(Psi F)) by A1, INSTALG1:25;
A5: (Psi F) . o = idsym (F . a) by A3, Th31;
then Args ((Psi F) . o),(MSAlg C2) = {{} } by Th34;
then A6: H # x = {} by A4, TARSKI:def 1;
reconsider h = id a as Morphism of a,a ;
( dom (id a) = a & cod (id a) = a ) by CAT_1:44;
then A7: id a in Hom a,a by CAT_1:18;
Args o,(MSAlg C1) = {{} } by A3, Th34;
then x = {} by TARSKI:def 1;
hence (H . (the_result_sort_of o)) . ((Den o,(MSAlg C1)) . x) = (H . (the_result_sort_of o)) . h by A3, 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 A7, CAT_1:131
.= id (F . a) by CAT_1:108
.= (Den ((Psi F) . o),(MSAlg C2)) . (H # x) by A5, A6, Def15
.= (Den o,((MSAlg C2) | (CatSign the carrier of C1),(Upsilon F),(Psi F))) . (H # x) by Th33, INSTALG1:24 ;
:: thesis:

end;

suppose A8: o `1 = 2 ; :: thesis:

let x be Element of Args o,(MSAlg C1); :: thesis:
consider a, b, c being Object of C1 such that
A9: o = compsym a,b,c by A8, Th27;
A10: (Psi F) . o = compsym (F . a),(F . b),(F . c) by A9, Th32;
consider g, h being Morphism of C1 such that
A11: x = <*g,h*> and
A12: dom h = a and
A13: cod h = b and
A14: dom g = b and
A15: cod g = c by A2, A9, Th39;
A16: ( g in Hom b,c & h in Hom a,b ) by A12, A13, A14, A15, CAT_1:18;
( dom (g * h) = a & cod (g * h) = c ) by A12, A13, A14, A15, CAT_1:42;
then A17: g * h in Hom a,c by CAT_1:18;
then reconsider gh = g * h as Morphism of a,c by CAT_1:def 7;
A18: ( dom (F . h) = F . a & cod (F . h) = F . b ) by A12, A13, CAT_1:109;
A19: ( dom (F . g) = F . b & cod (F . g) = F . c ) by A14, A15, CAT_1:109;
thus (H . (the_result_sort_of o)) . ((Den o,(MSAlg C1)) . x) = (H . (the_result_sort_of o)) . gh by A9, A11, A12, A13, A14, A15, Def15
.= (H . (homsym a,c)) . gh by A9, 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 A17, CAT_1:131
.= (F . g) * (F . h) by A13, A14, CAT_1:99
.= (Den ((Psi F) . o),(MSAlg C2)) . <*(F . g),(F . h)*> by A10, A18, A19, Def15
.= (Den ((Psi F) . o),(MSAlg C2)) . (H # x) by A9, A11, A16, Th40
.= (Den o,((MSAlg C2) | (CatSign the carrier of C1),(Upsilon F),(Psi F))) . (H # x) by Th33, INSTALG1:24 ; :: thesis:

end;

end;