let f, g be Function; :: thesis: ( f is one-to-one & g is one-to-one & ( for x1, x2 being set st x1 in dom g & x2 in (dom f) \ (dom g) holds
g . x1 <> f . x2 ) implies f +* g is one-to-one )
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: f +* g is one-to-one

now

let x11, x22 be set ; :: thesis: ( x11 in dom (f +* g) & x22 in dom (f +* g) & (f +* g) . x11 = (f +* g) . x22 implies x11 = x22 )
assume that
A4: x11 in dom (f +* g) and
A5: x22 in dom (f +* g) and
A6: (f +* g) . x11 = (f +* g) . x22 ; :: thesis: x11 = x22
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

per cases ( x11 in (dom f) \ (dom g) or x11 in dom g ) by A10, XBOOLE_0:def 3;

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

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

per cases ( x22 in (dom f) \ (dom g) or x22 in dom g ) by A8, XBOOLE_0:def 3;

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

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: verum

end;

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

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

end;

end;

end;

hence x11 = x22 ; :: thesis: verum

end;

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

now

per cases ( x22 in (dom f) \ (dom g) or x22 in dom g ) by A8, XBOOLE_0:def 3;

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

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: verum

end;

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

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: verum

end;

end;

end;

hence x11 = x22 ; :: thesis: verum

end;

end;

end;

hence x11 = x22 ; :: thesis: verum

end;

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