let f, g be Function; :: thesis: ( ( for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x ) implies ex h being Function st f \/ g = h )
assume A1: for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x ; :: thesis: ex h being Function st f \/ g = h
defpred S₁[ set , set ] means [$1,$2] in f \/ g;
A2: for x, y1, y2 being set st S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let x, y1, y2 be set ; :: thesis: ( S₁[x,y1] & S₁[x,y2] implies y1 = y2 )
assume that
A3: [x,y1] in f \/ g and
A4: [x,y2] in f \/ g ; :: thesis: y1 = y2

now

( [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, RELAT_1:def 4;

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 set holds
( [x,y] in h iff ( x in (dom f) \/ (dom g) & S₁[x,y] ) ) from FUNCT_1:sch 1(A2);
take h ; :: thesis: f \/ g = h
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [x,b₁] in f \/ g or [x,b₁] in h ) & ( not [x,b₁] in h or [x,b₁] in f \/ g ) )
let y be set ; :: thesis: ( ( not [x,y] in f \/ g or [x,y] in h ) & ( not [x,y] in h or [x,y] in f \/ g ) )
thus ( [x,y] in f \/ g implies [x,y] in h ) :: thesis: ( not [x,y] in h or [x,y] in f \/ g )

proof

assume A9: [x,y] in f \/ g ; :: thesis: [x,y] in h
then ( [x,y] in f or [x,y] in g ) by XBOOLE_0:def 3;
then ( x in dom f or x in dom g ) by RELAT_1:def 4;
then x in (dom f) \/ (dom g) by XBOOLE_0:def 3;
hence [x,y] in h by A8, A9; :: thesis: verum

end;

thus ( not [x,y] in h or [x,y] in f \/ g ) by A8; :: thesis: verum