let C1, C2 be Category; :: thesis: for F being Functor of C1,C2 ex 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)) & H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)) )

let F be Functor of C1,C2; :: thesis: ex 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)) & H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)) )

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 Th24;

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 Th28;

take H ; :: thesis: ( H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) & H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)) )

thus H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) ; :: thesis: H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))

let o be OperSymbol of (CatSign the carrier of C1); :: according to MSUALG_3:def 7 :: thesis: ( Args (o,(MSAlg C1)) = {} or for b_{1} being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b_{1}) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b_{1}) )

assume A2: Args (o,(MSAlg C1)) <> {} ; :: thesis: for b_{1} being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b_{1}) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b_{1})

( H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) & H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)) )

let F be Functor of C1,C2; :: thesis: ex 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)) & H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)) )

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 Th24;

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 Th28;

take H ; :: thesis: ( H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) & H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)) )

thus H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) ; :: thesis: H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))

let o be OperSymbol of (CatSign the carrier of C1); :: according to MSUALG_3:def 7 :: thesis: ( Args (o,(MSAlg C1)) = {} or for b

assume A2: Args (o,(MSAlg C1)) <> {} ; :: thesis: for b

per cases
( o `1 = 1 or o `1 = 2 )
by Th16;

end;

suppose
o `1 = 1
; :: thesis: for b_{1} being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b_{1}) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b_{1})

then consider a being Object of C1 such that

A3: o = idsym a by Th17;

let x be Element of Args (o,(MSAlg C1)); :: thesis: (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . x) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x)

A4: Args (((Psi F) . o),(MSAlg C2)) = Args (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)))) by A1, INSTALG1:24;

A5: (Psi F) . o = idsym (F . a) by A3, Th22;

then Args (((Psi F) . o),(MSAlg C2)) = {{}} by Th25;

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:58;

then A7: id a in Hom (a,a) ;

Args (o,(MSAlg C1)) = {{}} by A3, Th25;

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, Def13

.= (H . (homsym (a,a))) . h by A3, Def3

.= (F | ( the Sorts of (MSAlg C1) . (homsym (a,a)))) . h by Def1

.= (F | (Hom (a,a))) . h by Def13

.= (hom (F,a,a)) . h

.= F . h by A7, CAT_1:88

.= id (F . a) by CAT_1:71

.= (Den (((Psi F) . o),(MSAlg C2))) . (H # x) by A5, A6, Def13

.= (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x) by Th24, INSTALG1:23 ;

:: thesis: verum

end;A3: o = idsym a by Th17;

let x be Element of Args (o,(MSAlg C1)); :: thesis: (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . x) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x)

A4: Args (((Psi F) . o),(MSAlg C2)) = Args (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)))) by A1, INSTALG1:24;

A5: (Psi F) . o = idsym (F . a) by A3, Th22;

then Args (((Psi F) . o),(MSAlg C2)) = {{}} by Th25;

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:58;

then A7: id a in Hom (a,a) ;

Args (o,(MSAlg C1)) = {{}} by A3, Th25;

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, Def13

.= (H . (homsym (a,a))) . h by A3, Def3

.= (F | ( the Sorts of (MSAlg C1) . (homsym (a,a)))) . h by Def1

.= (F | (Hom (a,a))) . h by Def13

.= (hom (F,a,a)) . h

.= F . h by A7, CAT_1:88

.= id (F . a) by CAT_1:71

.= (Den (((Psi F) . o),(MSAlg C2))) . (H # x) by A5, A6, Def13

.= (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x) by Th24, INSTALG1:23 ;

:: thesis: verum

suppose A8:
o `1 = 2
; :: thesis: for b_{1} being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b_{1}) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b_{1})

let x be Element of Args (o,(MSAlg C1)); :: thesis: (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . x) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x)

consider a, b, c being Object of C1 such that

A9: o = compsym (a,b,c) by A8, Th18;

A10: (Psi F) . o = compsym ((F . a),(F . b),(F . c)) by A9, Th23;

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, Th29;

A16: ( g in Hom (b,c) & h in Hom (a,b) ) by A12, A13, A14, A15;

( dom (g (*) h) = a & cod (g (*) h) = c ) by A12, A13, A14, A15, CAT_1:17;

then A17: g (*) h in Hom (a,c) ;

then reconsider gh = g (*) h as Morphism of a,c by CAT_1:def 5;

A18: ( dom (F . h) = F . a & cod (F . h) = F . b ) by A12, A13, CAT_1:72;

A19: ( dom (F . g) = F . b & cod (F . g) = F . c ) by A14, A15, CAT_1:72;

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, Def13

.= (H . (homsym (a,c))) . gh by A9, Def3

.= (F | ( the Sorts of (MSAlg C1) . (homsym (a,c)))) . gh by Def1

.= (F | (Hom (a,c))) . gh by Def13

.= (hom (F,a,c)) . gh

.= F . gh by A17, CAT_1:88

.= (F . g) (*) (F . h) by A13, A14, CAT_1:64

.= (Den (((Psi F) . o),(MSAlg C2))) . <*(F . g),(F . h)*> by A10, A18, A19, Def13

.= (Den (((Psi F) . o),(MSAlg C2))) . (H # x) by A9, A11, A16, Th30

.= (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x) by Th24, INSTALG1:23 ; :: thesis: verum

end;consider a, b, c being Object of C1 such that

A9: o = compsym (a,b,c) by A8, Th18;

A10: (Psi F) . o = compsym ((F . a),(F . b),(F . c)) by A9, Th23;

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, Th29;

A16: ( g in Hom (b,c) & h in Hom (a,b) ) by A12, A13, A14, A15;

( dom (g (*) h) = a & cod (g (*) h) = c ) by A12, A13, A14, A15, CAT_1:17;

then A17: g (*) h in Hom (a,c) ;

then reconsider gh = g (*) h as Morphism of a,c by CAT_1:def 5;

A18: ( dom (F . h) = F . a & cod (F . h) = F . b ) by A12, A13, CAT_1:72;

A19: ( dom (F . g) = F . b & cod (F . g) = F . c ) by A14, A15, CAT_1:72;

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, Def13

.= (H . (homsym (a,c))) . gh by A9, Def3

.= (F | ( the Sorts of (MSAlg C1) . (homsym (a,c)))) . gh by Def1

.= (F | (Hom (a,c))) . gh by Def13

.= (hom (F,a,c)) . gh

.= F . gh by A17, CAT_1:88

.= (F . g) (*) (F . h) by A13, A14, CAT_1:64

.= (Den (((Psi F) . o),(MSAlg C2))) . <*(F . g),(F . h)*> by A10, A18, A19, Def13

.= (Den (((Psi F) . o),(MSAlg C2))) . (H # x) by A9, A11, A16, Th30

.= (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x) by Th24, INSTALG1:23 ; :: thesis: verum