set f = f1 +* f2;
set g = g1 +* g2;
set h = h1 +* h2;
A1: ( dom f1 = A & dom g1 = A & dom h1 = A & dom f2 = B & dom g2 = B & dom h2 = B ) by PARTFUN1:def 4;
h1 +* h2 is Function-yielding

proof

let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in dom (h1 +* h2) or (h1 +* h2) . x is set )
assume x in dom (h1 +* h2) ; :: thesis: (h1 +* h2) . x is set
then A2: x in A \/ B by PARTFUN1:def 4;
then ( ( x in A or x in B ) & ( not x in B or x in B ) ) by XBOOLE_0:def 3;
then ( ( (h1 +* h2) . x = h1 . x & h1 . x is Function ) or ( (h1 +* h2) . x = h2 . x & h2 . x is Function ) ) by A1, A2, FUNCT_4:def 1;
hence (h1 +* h2) . x is set ; :: thesis: verum

end;

then reconsider h = h1 +* h2 as ManySortedFunction of ;
h is ManySortedFunction of f1 +* f2,g1 +* g2

proof

let x be set ; :: according to PBOOLE:def 18 :: thesis: ( not x in A \/ B or h . x is Element of K21(K22(((f1 +* f2) . x),((g1 +* g2) . x))) )
assume A3: x in A \/ B ; :: thesis: h . x is Element of K21(K22(((f1 +* f2) . x),((g1 +* g2) . x)))
then ( ( x in A or x in B ) & ( not x in B or x in B ) ) by XBOOLE_0:def 3;
then ( ( h . x = h1 . x & h1 . x is Function of (f1 . x),(g1 . x) & (f1 +* f2) . x = f1 . x & (g1 +* g2) . x = g1 . x ) or ( h . x = h2 . x & h2 . x is Function of (f2 . x),(g2 . x) & (f1 +* f2) . x = f2 . x & (g1 +* g2) . x = g2 . x ) ) by A1, A3, FUNCT_4:def 1, PBOOLE:def 18;
hence h . x is Element of K21(K22(((f1 +* f2) . x),((g1 +* g2) . x))) ; :: thesis: verum

end;

hence h1 +* h2 is ManySortedFunction of f1 +* f2,g1 +* g2 ; :: thesis: verum