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;

f \/ g = f +* g by A2, FUNCT_4:31;

hence h is one-to-one by A1, A28, FUNCT_4:92; :: thesis: verum

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 A28:
( f is one-to-one & g is one-to-one & rng f misses rng g )
; :: thesis: 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 )

end;thus f is one-to-one :: thesis: ( g is one-to-one & rng f misses rng g )

proof

thus
g is one-to-one
:: thesis: rng f misses rng g
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;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

proof

thus
rng f misses rng g
:: thesis: verum
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;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

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;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

f \/ g = f +* g by A2, FUNCT_4:31;

hence h is one-to-one by A1, A28, FUNCT_4:92; :: thesis: verum