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 :: thesis: for x11, x22 being object st x11 in dom (f +* g) & x22 in dom (f +* g) & (f +* g) . x11 = (f +* g) . x22 holds
x11 = x22
let x11, x22 be object ; :: 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 ;
then A8: x22 in ((dom f) \ (dom g)) \/ (dom g) by XBOOLE_1:39;
A9: x11 in (dom f) \/ (dom g) by ;
then A10: x11 in ((dom f) \ (dom g)) \/ (dom g) by XBOOLE_1:39;
now :: thesis: x11 = x22
per cases ( x11 in (dom f) \ (dom g) or x11 in dom g ) by ;
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 ;
now :: thesis: ( ( x22 in (dom f) \ (dom g) & x11 = x22 ) or ( x22 in dom g & contradiction ) )
per cases ( x22 in (dom f) \ (dom g) or x22 in dom g ) by ;
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 ;
hence x11 = x22 by ; :: thesis: verum
end;
end;
end;
hence x11 = x22 ; :: thesis: verum
end;
suppose A15: x11 in dom g ; :: thesis: x11 = x22
now :: thesis: ( ( x22 in (dom f) \ (dom g) & contradiction ) or ( x22 in dom g & x11 = x22 ) )
per cases ( x22 in (dom f) \ (dom g) or x22 in dom g ) by ;
case A16: x22 in (dom f) \ (dom g) ; :: thesis: contradiction
end;
case A18: x22 in dom g ; :: thesis: x11 = x22
then (f +* g) . x22 = g . x22 by ;
then g . x11 = g . x22 by ;
hence x11 = x22 by ; :: 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