set f = f1 +* f2;
set g = g1 +* g2;
set h = h1 +* h2;
A1: dom g1 = A by PARTFUN1:def 2;
A2: dom f2 = B by PARTFUN1:def 2;
A3: dom g2 = B by PARTFUN1:def 2;
A4: dom h2 = B by PARTFUN1:def 2;
A5: dom h1 = A by PARTFUN1:def 2;
reconsider h = h1 +* h2 as ManySortedFunction of A \/ B ;
A6: dom f1 = A by PARTFUN1:def 2;
h is ManySortedFunction of f1 +* f2,g1 +* g2

proof

let x be object ; :: according to PBOOLE:def 15 :: thesis: ( not x in A \/ B or h . x is Element of K19(K20(((f1 +* f2) . x),((g1 +* g2) . x))) )
A7: ( not x in B or x in B ) ;
assume A8: x in A \/ B ; :: thesis: h . x is Element of K19(K20(((f1 +* f2) . x),((g1 +* g2) . x)))
then ( x in A 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 A6, A1, A5, A2, A3, A4, A8, A7, FUNCT_4:def 1, PBOOLE:def 15;
hence h . x is Element of K19(K20(((f1 +* f2) . x),((g1 +* g2) . x))) ; :: thesis: verum

end;

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