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 ;
PBOOLE:def 15 ( 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
;
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)))
;
verum
end;
hence
h1 +* h2 is ManySortedFunction of f1 +* f2,g1 +* g2
; verum