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 object ; :: according to PBOOLE:def 15 :: 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 Th15;
Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2 by Th24;
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:15;
(Upsilon F) . s = homsym ((F . a),(F . b)) by A1, Th21;
then A3: the Sorts of (MSAlg C2) . ((Upsilon F) . s) = Hom ((F . a),(F . b)) by Def13;
A4: the Sorts of (MSAlg C1) . s = Hom (a,b) by A1, Def13;
(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;
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