let f, g, h 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 that
A1: h = f \/ g and
A2: 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 ) )
A3: dom h = (dom f) \/ (dom g) by A1, XTUPLE_0:23;

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

assume A4: 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 object such that
A5: x1 in dom f and
A6: x2 in dom f and
A7: ( f . x1 = f . x2 & x1 <> x2 ) ;
A8: x2 in dom h by A3, A6, XBOOLE_0:def 3;
[x2,(f . x2)] in f by A6, FUNCT_1:def 2;
then [x2,(f . x2)] in h by A1, XBOOLE_0:def 3;
then A9: f . x2 = h . x2 by A8, FUNCT_1:def 2;
A10: x1 in dom h by A3, A5, XBOOLE_0:def 3;
[x1,(f . x1)] in f by A5, FUNCT_1:def 2;
then [x1,(f . x1)] in h by A1, XBOOLE_0:def 3;
then f . x1 = h . x1 by A10, FUNCT_1:def 2;
hence contradiction by A4, A7, A10, A8, A9; :: 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 object such that
A11: x1 in dom g and
A12: x2 in dom g and
A13: ( g . x1 = g . x2 & x1 <> x2 ) ;
A14: x2 in dom h by A3, A12, XBOOLE_0:def 3;
[x2,(g . x2)] in g by A12, FUNCT_1:def 2;
then [x2,(g . x2)] in h by A1, XBOOLE_0:def 3;
then A15: g . x2 = h . x2 by A14, FUNCT_1:def 2;
A16: x1 in dom h by A3, A11, XBOOLE_0:def 3;
[x1,(g . x1)] in g by A11, FUNCT_1:def 2;
then [x1,(g . x1)] in h by A1, XBOOLE_0:def 3;
then g . x1 = h . x1 by A16, FUNCT_1:def 2;
hence contradiction by A4, A13, A16, A14, A15; :: 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 object such that
A17: hx in rng f and
A18: hx in rng g by XBOOLE_0:3;
consider x1 being object such that
A19: x1 in dom f and
A20: hx = f . x1 by A17, FUNCT_1:def 3;
A21: x1 in dom h by A3, A19, XBOOLE_0:def 3;
consider x2 being object such that
A22: x2 in dom g and
A23: hx = g . x2 by A18, FUNCT_1:def 3;
A24: x2 in dom h by A3, A22, XBOOLE_0:def 3;
A25: hx is set by TARSKI:1;
[x2,hx] in g by A22, A23, FUNCT_1:def 2;
then [x2,hx] in h by A1, XBOOLE_0:def 3;
then A26: h . x2 = hx by A24, FUNCT_1:def 2, A25;
A27: x1 <> x2 by A2, A19, A22, XBOOLE_0:3;
[x1,hx] in f by A19, A20, FUNCT_1:def 2;
then [x1,hx] in h by A1, XBOOLE_0:def 3;
then h . x1 = hx by A21, FUNCT_1:def 2, A25;
hence contradiction by A4, A27, A21, A24, A26; :: thesis: verum

end;

end;

assume A28: ( 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 A2, FUNCT_4:31;
hence h is one-to-one by A1, A28, FUNCT_4:92; :: thesis: verum