let f, g be Function; ( ( 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
; 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 ;
( S1[x,y1] & S1[x,y2] implies y1 = y2 )
assume that A3:
[x,y1] in f \/ g
and A4:
[x,y2] in f \/ g
;
y1 = y2
hence
y1 = y2
;
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 ;
RELAT_1:def 2 ( ( 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;
( not [x,y] in f \/ g or [x,y] in h )
assume A9:
[x,y] in f \/ g
;
[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;
verum
end;
hence
f \/ g is Function
; verum