let X, Y be set ; :: thesis: for C, D being non empty set

for f being PartFunc of C,D st f | X is V8() & f | Y is V8() & X /\ Y meets dom f holds

f | (X \/ Y) is V8()

let C, D be non empty set ; :: thesis: for f being PartFunc of C,D st f | X is V8() & f | Y is V8() & X /\ Y meets dom f holds

f | (X \/ Y) is V8()

let f be PartFunc of C,D; :: thesis: ( f | X is V8() & f | Y is V8() & X /\ Y meets dom f implies f | (X \/ Y) is V8() )

assume that

A1: f | X is V8() and

A2: f | Y is V8() and

A3: (X /\ Y) /\ (dom f) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: f | (X \/ Y) is V8()

consider d1 being Element of D such that

A4: for c being Element of C st c in X /\ (dom f) holds

f /. c = d1 by A1, Th35;

set x = the Element of (X /\ Y) /\ (dom f);

A5: the Element of (X /\ Y) /\ (dom f) in X /\ Y by A3, XBOOLE_0:def 4;

A6: the Element of (X /\ Y) /\ (dom f) in dom f by A3, XBOOLE_0:def 4;

then reconsider x = the Element of (X /\ Y) /\ (dom f) as Element of C ;

x in Y by A5, XBOOLE_0:def 4;

then A7: x in Y /\ (dom f) by A6, XBOOLE_0:def 4;

consider d2 being Element of D such that

A8: for c being Element of C st c in Y /\ (dom f) holds

f /. c = d2 by A2, Th35;

x in X by A5, XBOOLE_0:def 4;

then x in X /\ (dom f) by A6, XBOOLE_0:def 4;

then f /. x = d1 by A4;

then A9: d1 = d2 by A8, A7;

take d1 ; :: according to PARTFUN2:def 1 :: thesis: for c being Element of C st c in dom (f | (X \/ Y)) holds

(f | (X \/ Y)) . c = d1

let c be Element of C; :: thesis: ( c in dom (f | (X \/ Y)) implies (f | (X \/ Y)) . c = d1 )

assume A10: c in dom (f | (X \/ Y)) ; :: thesis: (f | (X \/ Y)) . c = d1

then A11: c in (X \/ Y) /\ (dom f) by RELAT_1:61;

then A12: c in dom f by XBOOLE_0:def 4;

A13: c in X \/ Y by A11, XBOOLE_0:def 4;

hence (f | (X \/ Y)) . c = d1 by A10, PARTFUN1:def 6; :: thesis: verum

for f being PartFunc of C,D st f | X is V8() & f | Y is V8() & X /\ Y meets dom f holds

f | (X \/ Y) is V8()

let C, D be non empty set ; :: thesis: for f being PartFunc of C,D st f | X is V8() & f | Y is V8() & X /\ Y meets dom f holds

f | (X \/ Y) is V8()

let f be PartFunc of C,D; :: thesis: ( f | X is V8() & f | Y is V8() & X /\ Y meets dom f implies f | (X \/ Y) is V8() )

assume that

A1: f | X is V8() and

A2: f | Y is V8() and

A3: (X /\ Y) /\ (dom f) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: f | (X \/ Y) is V8()

consider d1 being Element of D such that

A4: for c being Element of C st c in X /\ (dom f) holds

f /. c = d1 by A1, Th35;

set x = the Element of (X /\ Y) /\ (dom f);

A5: the Element of (X /\ Y) /\ (dom f) in X /\ Y by A3, XBOOLE_0:def 4;

A6: the Element of (X /\ Y) /\ (dom f) in dom f by A3, XBOOLE_0:def 4;

then reconsider x = the Element of (X /\ Y) /\ (dom f) as Element of C ;

x in Y by A5, XBOOLE_0:def 4;

then A7: x in Y /\ (dom f) by A6, XBOOLE_0:def 4;

consider d2 being Element of D such that

A8: for c being Element of C st c in Y /\ (dom f) holds

f /. c = d2 by A2, Th35;

x in X by A5, XBOOLE_0:def 4;

then x in X /\ (dom f) by A6, XBOOLE_0:def 4;

then f /. x = d1 by A4;

then A9: d1 = d2 by A8, A7;

take d1 ; :: according to PARTFUN2:def 1 :: thesis: for c being Element of C st c in dom (f | (X \/ Y)) holds

(f | (X \/ Y)) . c = d1

let c be Element of C; :: thesis: ( c in dom (f | (X \/ Y)) implies (f | (X \/ Y)) . c = d1 )

assume A10: c in dom (f | (X \/ Y)) ; :: thesis: (f | (X \/ Y)) . c = d1

then A11: c in (X \/ Y) /\ (dom f) by RELAT_1:61;

then A12: c in dom f by XBOOLE_0:def 4;

A13: c in X \/ Y by A11, XBOOLE_0:def 4;

now :: thesis: f /. c = d1

then
(f | (X \/ Y)) /. c = d1
by A11, Th16;end;

hence (f | (X \/ Y)) . c = d1 by A10, PARTFUN1:def 6; :: thesis: verum