let f, g, h be Function; :: thesis: ( f is one-to-one & g is one-to-one & h = f \/ g & rng f misses rng g implies h is one-to-one )
assume that
A1: ( f is one-to-one & g is one-to-one ) and
A2: h = f \/ g and
A3: (rng f) /\ (rng g) = {} ; :: according to XBOOLE_0:def 7 :: thesis: h is one-to-one

now :: thesis: for x1, x2 being object st x1 in dom h & x2 in dom h & h . x1 = h . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom h & x2 in dom h & h . x1 = h . x2 implies x1 = x2 )
assume that
A4: ( x1 in dom h & x2 in dom h ) and
A5: h . x1 = h . x2 ; :: thesis: x1 = x2

A6: now :: thesis: ( ( ( x1 in dom f & x2 in dom g ) or ( x1 in dom g & x2 in dom f ) ) implies x1 = x2 )

assume ( ( x1 in dom f & x2 in dom g ) or ( x1 in dom g & x2 in dom f ) ) ; :: thesis: x1 = x2
then ( ( h . x1 = f . x1 & h . x2 = g . x2 & f . x1 <> g . x2 ) or ( h . x1 = g . x1 & h . x2 = f . x2 & f . x2 <> g . x1 ) ) by A2, A3, Lm1, Th15;
hence x1 = x2 by A5; :: thesis: verum

end;

A7: ( x1 in dom g & x2 in dom g implies ( h . x1 = g . x1 & h . x2 = g . x2 ) ) by A2, Th15;
( x1 in dom f & x2 in dom f implies ( h . x1 = f . x1 & h . x2 = f . x2 ) ) by A2, Th15;
then ( ( ( x1 in dom f & x2 in dom f ) or ( x1 in dom g & x2 in dom g ) ) implies x1 = x2 ) by A1, A5, A7;
hence x1 = x2 by A2, A4, A6, Lm3; :: thesis: verum

end;

hence h is one-to-one ; :: thesis: verum