let f, g be Function; :: thesis: for a being set st f is one-to-one & g is one-to-one & (dom f) /\ (dom g) = {a} & (rng f) /\ (rng g) = {(f . a)} holds
f +* g is one-to-one
let a be set ; :: thesis: ( f is one-to-one & g is one-to-one & (dom f) /\ (dom g) = {a} & (rng f) /\ (rng g) = {(f . a)} implies f +* g is one-to-one )
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: (dom f) /\ (dom g) = {a} and
A4: (rng f) /\ (rng g) = {(f . a)} ; :: thesis: f +* 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

proof

{a} c= dom g by A3, XBOOLE_1:17;
then A5: a in dom g by ZFMISC_1:31;
{a} c= dom f by A3, XBOOLE_1:17;
then A6: a in dom f by ZFMISC_1:31;
let x1, x2 be set ; :: thesis: ( x1 in dom g & x2 in (dom f) \ (dom g) implies g . x1 <> f . x2 )
assume that
A7: x1 in dom g and
A8: x2 in (dom f) \ (dom g) ; :: thesis: g . x1 <> f . x2
A9: f . x2 in rng f by A8, FUNCT_1:3;
assume A10: g . x1 = f . x2 ; :: thesis: contradiction
g . x1 in rng g by A7, FUNCT_1:3;
then f . x2 in (rng f) /\ (rng g) by A9, A10, XBOOLE_0:def 4;
then f . x2 = f . a by A4, TARSKI:def 1;
then x2 = a by A1, A8, A6, FUNCT_1:def 4;
then dom g meets (dom f) \ (dom g) by A8, A5, XBOOLE_0:3;
hence contradiction by XBOOLE_1:79; :: thesis: verum

end;

hence f +* g is one-to-one by A1, A2, TOPMETR2:1; :: thesis: verum