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

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

end;

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