let C1, C2 be Category; :: thesis: for F being Functor of C1,C2 holds F -MSF the carrier of (CatSign the carrier of C1),the Sorts of (MSAlg C1) is ManySortedFunction of (MSAlg C1),((MSAlg C2) | (CatSign the carrier of C1),(Upsilon F),(Psi F))
let F be Functor of C1,C2; :: thesis: F -MSF the carrier of (CatSign the carrier of C1),the Sorts of (MSAlg C1) is ManySortedFunction of (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);
set H = F -MSF the carrier of (CatSign the carrier of C1),the Sorts of (MSAlg C1);
let i be set ; :: according to PBOOLE:def 18 :: thesis: ( not i in the carrier of (CatSign the carrier of C1) or (F -MSF the carrier of (CatSign the carrier of C1),the Sorts of (MSAlg C1)) . i is Element of bool [:(the Sorts of (MSAlg C1) . i),(the Sorts of ((MSAlg C2) | (CatSign the carrier of C1),(Upsilon F),(Psi F)) . i):] )
assume i in the carrier of (CatSign the carrier of C1) ; :: thesis: (F -MSF the carrier of (CatSign the carrier of C1),the Sorts of (MSAlg C1)) . i is Element of bool [:(the Sorts of (MSAlg C1) . i),(the Sorts of ((MSAlg C2) | (CatSign the carrier of C1),(Upsilon F),(Psi F)) . i):]
then reconsider s = i as SortSymbol of (CatSign the carrier of C1) ;
consider a, b being Object of C1 such that
A1: s = homsym a,b by Th24;
Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2 by Th33;
then the Sorts of ((MSAlg C2) | (CatSign the carrier of C1),(Upsilon F),(Psi F)) = the Sorts of (MSAlg C2) * (Upsilon F) by INSTALG1:def 3;
then A2: the Sorts of (MSAlg C2) . ((Upsilon F) . s) = the Sorts of ((MSAlg C2) | (CatSign the carrier of C1),(Upsilon F),(Psi F)) . s by FUNCT_2:21;
(Upsilon F) . s = homsym (F . a),(F . b) by A1, Th30;
then A3: the Sorts of (MSAlg C2) . ((Upsilon F) . s) = Hom (F . a),(F . b) by Def15;
A4: the Sorts of (MSAlg C1) . s = Hom a,b by A1, Def15;
(F -MSF the carrier of (CatSign the carrier of C1),the Sorts of (MSAlg C1)) . s = F | (the Sorts of (MSAlg C1) . s) by Def1;
then (F -MSF the carrier of (CatSign the carrier of C1),the Sorts of (MSAlg C1)) . s = hom F,a,b by A4, CAT_1:def 25;
hence (F -MSF the carrier of (CatSign the carrier of C1),the Sorts of (MSAlg C1)) . i is Element of bool [:(the Sorts of (MSAlg C1) . i),(the Sorts of ((MSAlg C2) | (CatSign the carrier of C1),(Upsilon F),(Psi F)) . i):] by A2, A4, A3; :: thesis: verum