let h, f, g be Function; :: thesis: ( h = f \/ g & dom f misses dom g implies ( h is one-to-one iff ( f is one-to-one & g is one-to-one & rng f misses rng g ) ) )
assume A1: ( h = f \/ g & dom f misses dom g ) ; :: thesis: ( h is one-to-one iff ( f is one-to-one & g is one-to-one & rng f misses rng g ) )
then A2: dom h = (dom f) \/ (dom g) by RELAT_1:13;

hereby :: thesis: ( f is one-to-one & g is one-to-one & rng f misses rng g implies h is one-to-one )

assume A3: h is one-to-one ; :: thesis: ( f is one-to-one & g is one-to-one & rng f misses rng g )
thus f is one-to-one :: thesis: ( g is one-to-one & rng f misses rng g )

proof

assume not f is one-to-one ; :: thesis: contradiction
then consider x1, x2 being set such that
A4: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 & x1 <> x2 ) by FUNCT_1:def 8;
( [x1,(f . x1)] in f & [x2,(f . x2)] in f ) by A4, FUNCT_1:def 4;
then A5: ( [x1,(f . x1)] in h & [x2,(f . x2)] in h ) by A1, XBOOLE_0:def 3;
A6: ( x1 in dom h & x2 in dom h ) by A2, A4, XBOOLE_0:def 3;
then ( f . x1 = h . x1 & f . x2 = h . x2 ) by A5, FUNCT_1:def 4;
hence contradiction by A3, A4, A6, FUNCT_1:def 8; :: thesis: verum

end;

thus g is one-to-one :: thesis: rng f misses rng g

proof

assume not g is one-to-one ; :: thesis: contradiction
then consider x1, x2 being set such that
A7: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 & x1 <> x2 ) by FUNCT_1:def 8;
( [x1,(g . x1)] in g & [x2,(g . x2)] in g ) by A7, FUNCT_1:def 4;
then A8: ( [x1,(g . x1)] in h & [x2,(g . x2)] in h ) by A1, XBOOLE_0:def 3;
A9: ( x1 in dom h & x2 in dom h ) by A2, A7, XBOOLE_0:def 3;
then ( g . x1 = h . x1 & g . x2 = h . x2 ) by A8, FUNCT_1:def 4;
hence contradiction by A3, A7, A9, FUNCT_1:def 8; :: thesis: verum

end;

thus rng f misses rng g :: thesis: verum

proof

assume not rng f misses rng g ; :: thesis: contradiction
then consider hx being set such that
A10: ( hx in rng f & hx in rng g ) by XBOOLE_0:3;
consider x1 being set such that
A11: ( x1 in dom f & hx = f . x1 ) by A10, FUNCT_1:def 5;
consider x2 being set such that
A12: ( x2 in dom g & hx = g . x2 ) by A10, FUNCT_1:def 5;
A13: x1 <> x2 by A1, A11, A12, XBOOLE_0:3;
( [x1,hx] in f & [x2,hx] in g ) by A11, A12, FUNCT_1:def 4;
then A14: ( [x1,hx] in h & [x2,hx] in h ) by A1, XBOOLE_0:def 3;
A15: ( x1 in dom h & x2 in dom h ) by A2, A11, A12, XBOOLE_0:def 3;
then ( h . x1 = hx & h . x2 = hx ) by A14, FUNCT_1:def 4;
hence contradiction by A3, A13, A15, FUNCT_1:def 8; :: thesis: verum

end;

end;

assume A16: ( f is one-to-one & g is one-to-one & rng f misses rng g ) ; :: thesis: h is one-to-one
f \/ g = f +* g by A1, FUNCT_4:32;
hence h is one-to-one by A1, A16, FUNCT_4:98; :: thesis: verum