let X, Y be set ; :: thesis: for C, D being non empty set
for f being PartFunc of C,D st f | X is constant & f | Y is constant & X /\ Y meets dom f holds
f | (X \/ Y) is constant
let C, D be non empty set ; :: thesis: for f being PartFunc of C,D st f | X is constant & f | Y is constant & X /\ Y meets dom f holds
f | (X \/ Y) is constant
let f be PartFunc of C,D; :: thesis: ( f | X is constant & f | Y is constant & X /\ Y meets dom f implies f | (X \/ Y) is constant )
assume A1: ( f | X is constant & f | Y is constant & (X /\ Y) /\ (dom f) <> {} ) ; :: according to XBOOLE_0:def 7 :: thesis: f | (X \/ Y) is constant
then consider d1 being Element of D such that
A2: for c being Element of C st c in X /\ (dom f) holds
f /. c = d1 by Thx;
consider d2 being Element of D such that
A3: for c being Element of C st c in Y /\ (dom f) holds
f /. c = d2 by A1, Thx;
consider x being Element of (X /\ Y) /\ (dom f);
A4: ( x in X /\ Y & x in dom f ) by A1, XBOOLE_0:def 4;
then reconsider x = x as Element of C ;
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
( x in X & x in dom f ) by A4, XBOOLE_0:def 4;
then x in X /\ (dom f) by XBOOLE_0:def 4;
then A5: f /. x = d1 by A2;
( x in Y & x in dom f ) by A4, XBOOLE_0:def 4;
then x in Y /\ (dom f) by XBOOLE_0:def 4;
then A6: d1 = d2 by A3, A5;
let c be Element of C; :: thesis: ( c in dom (f | (X \/ Y)) implies (f | (X \/ Y)) . c = d1 )
assume Z: c in dom (f | (X \/ Y)) ; :: thesis: (f | (X \/ Y)) . c = d1
then X: c in (X \/ Y) /\ (dom f) by RELAT_1:90;
then A7: ( c in X \/ Y & c in dom f ) by XBOOLE_0:def 4;

now

per cases ( c in X or c in Y ) by A7, XBOOLE_0:def 3;

suppose c in X ; :: thesis: f /. c = d1

then c in X /\ (dom f) by A7, XBOOLE_0:def 4;
hence f /. c = d1 by A2; :: thesis: verum

end;

suppose c in Y ; :: thesis: f /. c = d1

then c in Y /\ (dom f) by A7, XBOOLE_0:def 4;
hence f /. c = d1 by A3, A6; :: thesis: verum

end;

end;

end;

then (f | (X \/ Y)) /. c = d1 by X, Th34;
hence (f | (X \/ Y)) . c = d1 by Z, PARTFUN1:def 8; :: thesis: verum