let f, g be Function; :: thesis: ( ( for x being object st x in (dom f) /\ (dom g) holds
f . x = g . x ) implies f \/ g is Function )
assume A1: for x being object st x in (dom f) /\ (dom g) holds
f . x = g . x ; :: thesis: f \/ g is Function
defpred S1[ object , object ] means [$1,$2] in f \/ g;
A2: for x, y1, y2 being object st S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let x, y1, y2 be object ; :: thesis: ( S1[x,y1] & S1[x,y2] implies y1 = y2 )
assume that
A3: [x,y1] in f \/ g and
A4: [x,y2] in f \/ g ; :: thesis: y1 = y2
now :: thesis: y1 = y2
( [x,y1] in f or [x,y1] in g ) by A3, XBOOLE_0:def 3;
then A5: ( ( x in dom f & f . x = y1 ) or ( x in dom g & g . x = y1 ) ) by FUNCT_1:1;
A6: ( [x,y2] in f or [x,y2] in g ) by A4, XBOOLE_0:def 3;
then A7: ( ( x in dom f & f . x = y2 ) or ( x in dom g & g . x = y2 ) ) by FUNCT_1:1;
per cases ( ( x in dom f & x in dom g ) or ( x in dom f & not x in dom g ) or ( not x in dom f & x in dom g ) ) by A6, XTUPLE_0:def 12;
suppose ( x in dom f & x in dom g ) ; :: thesis: y1 = y2
then x in (dom f) /\ (dom g) by XBOOLE_0:def 4;
hence y1 = y2 by A1, A5, A7; :: thesis: verum
end;
suppose ( x in dom f & not x in dom g ) ; :: thesis: y1 = y2
hence y1 = y2 by A6, A5, FUNCT_1:1; :: thesis: verum
end;
suppose ( not x in dom f & x in dom g ) ; :: thesis: y1 = y2
hence y1 = y2 by A6, A5, FUNCT_1:1; :: thesis: verum
end;
end;
end;
hence y1 = y2 ; :: thesis: verum
end;
consider h being Function such that
A8: for x, y being object holds
( [x,y] in h iff ( x in (dom f) \/ (dom g) & S1[x,y] ) ) from FUNCT_1:sch 1(A2);
 h = f \/ g
proof
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in h or [x,y] in f \/ g ) & ( not [x,y] in f \/ g or [x,y] in h ) )
thus ( [x,y] in h implies [x,y] in f \/ g ) by A8; :: thesis: ( not [x,y] in f \/ g or [x,y] in h )
assume A9: [x,y] in f \/ g ; :: thesis: [x,y] in h
( [x,y] in f or [x,y] in g ) by A9, XBOOLE_0:def 3;
then ( x in dom f or x in dom g ) by XTUPLE_0:def 12;
then x in (dom f) \/ (dom g) by XBOOLE_0:def 3;
hence [x,y] in h by A8, A9; :: thesis: verum
end;
hence f \/ g is Function ; :: thesis: verum