let f, g be Function; ( dom f misses dom g implies f \/ g is Function )
assume A1:
(dom f) /\ (dom g) = {}
; XBOOLE_0:def 7 f \/ g is Function
now ( ( 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;
for x, y1, y2 being object st [x,y1] in f \/ g & [x,y2] in f \/ g holds
y1 = y2let x,
y1,
y2 be
object ;
( [x,y1] in f \/ g & [x,y2] in f \/ g implies y1 = y2 )assume
[x,y1] in f \/ g
;
( [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
;
y1 = y2then 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;
verum end;
hence
f \/ g is Function
by FUNCT_1:def 1; verum