let f, g be Function; :: thesis: ( dom f misses dom g implies f \/ g is Function )
assume A1: (dom f) /\ (dom g) = {} ; :: according to XBOOLE_0:def 7 :: thesis: f \/ g is Function

now :: thesis: ( ( for p being object st p in f \/ g holds
ex x, y being object st [x,y] = p ) & ( for x, y1, y2 being object st [x,y1] in f \/ g & [x,y2] in f \/ g holds
y1 = y2 ) )

thus for p being object st p in f \/ g holds
ex x, y being object st [x,y] = p by RELAT_1:def 1; :: thesis: for x, y1, y2 being object st [x,y1] in f \/ g & [x,y2] in f \/ g holds
y1 = y2
let x, y1, y2 be object ; :: thesis: ( [x,y1] in f \/ g & [x,y2] in f \/ g implies y1 = y2 )
assume [x,y1] in f \/ g ; :: thesis: ( [x,y2] in f \/ g implies y1 = y2 )
then A2: ( [x,y1] in f or [x,y1] in g ) by XBOOLE_0:def 3;
assume [x,y2] in f \/ g ; :: thesis: y1 = y2
then A3: ( [x,y2] in f or [x,y2] in g ) by XBOOLE_0:def 3;
( not x in dom f or not x in dom g ) by A1, XBOOLE_0:def 4;
hence y1 = y2 by A2, A3, FUNCT_1:def 1, XTUPLE_0:def 12; :: thesis: verum

end;

hence f \/ g is Function by FUNCT_1:def 1; :: thesis: verum