let f, g be Function; :: thesis:
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: for x1, x2 being set st x1 in dom g & x2 in (dom f) \ (dom g) holds
g . x1 <> f . x2 ; :: thesis:

now :: thesis:

let x11, x22 be object ; :: thesis:
assume that
A4: x11 in dom (f +* g) and
A5: x22 in dom (f +* g) and
A6: (f +* g) . x11 = (f +* g) . x22 ; :: thesis:
A7: x22 in (dom f) \/ (dom g) by A5, FUNCT_4:def 1;
then A8: x22 in ((dom f) \ (dom g)) \/ (dom g) by XBOOLE_1:39;
A9: x11 in (dom f) \/ (dom g) by A4, FUNCT_4:def 1;
then A10: x11 in ((dom f) \ (dom g)) \/ (dom g) by XBOOLE_1:39;

now :: thesis:

per cases by A10, XBOOLE_0:def 3;

suppose A11: x11 in (dom f) \ (dom g) ; :: thesis:

then not x11 in dom g by XBOOLE_0:def 5;
then A12: (f +* g) . x11 = f . x11 by A9, FUNCT_4:def 1;

now :: thesis:

per cases by A8, XBOOLE_0:def 3;

case A13: x22 in (dom f) \ (dom g) ; :: thesis:

then not x22 in dom g by XBOOLE_0:def 5;
then f . x11 = f . x22 by A6, A7, A12, FUNCT_4:def 1;
hence x11 = x22 by A1, A11, A13, FUNCT_1:def 4; :: thesis:

end;

case A14: x22 in dom g ; :: thesis:

then g . x22 <> f . x11 by A3, A11;
hence contradiction by A6, A7, A12, A14, FUNCT_4:def 1; :: thesis:

end;

end;

end;

hence x11 = x22 ; :: thesis:

end;

suppose A15: x11 in dom g ; :: thesis:

now :: thesis:

per cases by A8, XBOOLE_0:def 3;

case A16: x22 in (dom f) \ (dom g) ; :: thesis:

then not x22 in dom g by XBOOLE_0:def 5;
then A17: (f +* g) . x22 = f . x22 by A7, FUNCT_4:def 1;
g . x11 <> f . x22 by A3, A15, A16;
hence contradiction by A6, A9, A15, A17, FUNCT_4:def 1; :: thesis:

end;

case A18: x22 in dom g ; :: thesis:

then (f +* g) . x22 = g . x22 by A7, FUNCT_4:def 1;
then g . x11 = g . x22 by A6, A9, A15, FUNCT_4:def 1;
hence x11 = x22 by A2, A15, A18, FUNCT_1:def 4; :: thesis:

end;

end;

end;

hence x11 = x22 ; :: thesis:

end;

end;

end;

hence x11 = x22 ; :: thesis:

end;

hence f +* g is one-to-one by FUNCT_1:def 4; :: thesis: