let f, g be Function; :: thesis: ( f is one-to-one & 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 ) implies f +* g is one-to-one )

assume that

A1: f is one-to-one and

A2: g is one-to-one and

A3: for x1, x2 being set st x1 in dom g & x2 in (dom f) \ (dom g) holds

g . x1 <> f . x2 ; :: thesis: f +* g is one-to-one

g . x1 <> f . x2 ) implies f +* g is one-to-one )

assume that

A1: f is one-to-one and

A2: g is one-to-one and

A3: for x1, x2 being set st x1 in dom g & x2 in (dom f) \ (dom g) holds

g . x1 <> f . x2 ; :: thesis: f +* g is one-to-one

now :: thesis: for x11, x22 being object st x11 in dom (f +* g) & x22 in dom (f +* g) & (f +* g) . x11 = (f +* g) . x22 holds

x11 = x22

hence
f +* g is one-to-one
by FUNCT_1:def 4; :: thesis: verumx11 = x22

let x11, x22 be object ; :: thesis: ( x11 in dom (f +* g) & x22 in dom (f +* g) & (f +* g) . x11 = (f +* g) . x22 implies x11 = x22 )

assume that

A4: x11 in dom (f +* g) and

A5: x22 in dom (f +* g) and

A6: (f +* g) . x11 = (f +* g) . x22 ; :: thesis: x11 = x22

A7: x22 in (dom f) \/ (dom g) by A5, FUNCT_4:def 1;

then A8: x22 in ((dom f) \ (dom g)) \/ (dom g) by XBOOLE_1:39;

A9: x11 in (dom f) \/ (dom g) by A4, FUNCT_4:def 1;

then A10: x11 in ((dom f) \ (dom g)) \/ (dom g) by XBOOLE_1:39;

end;assume that

A4: x11 in dom (f +* g) and

A5: x22 in dom (f +* g) and

A6: (f +* g) . x11 = (f +* g) . x22 ; :: thesis: x11 = x22

A7: x22 in (dom f) \/ (dom g) by A5, FUNCT_4:def 1;

then A8: x22 in ((dom f) \ (dom g)) \/ (dom g) by XBOOLE_1:39;

A9: x11 in (dom f) \/ (dom g) by A4, FUNCT_4:def 1;

then A10: x11 in ((dom f) \ (dom g)) \/ (dom g) by XBOOLE_1:39;

now :: thesis: x11 = x22end;

hence
x11 = x22
; :: thesis: verumper cases
( x11 in (dom f) \ (dom g) or x11 in dom g )
by A10, XBOOLE_0:def 3;

end;

suppose A11:
x11 in (dom f) \ (dom g)
; :: thesis: x11 = x22

then
not x11 in dom g
by XBOOLE_0:def 5;

then A12: (f +* g) . x11 = f . x11 by A9, FUNCT_4:def 1;

end;then A12: (f +* g) . x11 = f . x11 by A9, FUNCT_4:def 1;

now :: thesis: ( ( x22 in (dom f) \ (dom g) & x11 = x22 ) or ( x22 in dom g & contradiction ) )end;

hence
x11 = x22
; :: thesis: verumper cases
( x22 in (dom f) \ (dom g) or x22 in dom g )
by A8, XBOOLE_0:def 3;

end;

case A13:
x22 in (dom f) \ (dom g)
; :: thesis: x11 = x22

then
not x22 in dom g
by XBOOLE_0:def 5;

then f . x11 = f . x22 by A6, A7, A12, FUNCT_4:def 1;

hence x11 = x22 by A1, A11, A13, FUNCT_1:def 4; :: thesis: verum

end;then f . x11 = f . x22 by A6, A7, A12, FUNCT_4:def 1;

hence x11 = x22 by A1, A11, A13, FUNCT_1:def 4; :: thesis: verum

case A14:
x22 in dom g
; :: thesis: contradiction

then
g . x22 <> f . x11
by A3, A11;

hence contradiction by A6, A7, A12, A14, FUNCT_4:def 1; :: thesis: verum

end;hence contradiction by A6, A7, A12, A14, FUNCT_4:def 1; :: thesis: verum

suppose A15:
x11 in dom g
; :: thesis: x11 = x22

end;

now :: thesis: ( ( x22 in (dom f) \ (dom g) & contradiction ) or ( x22 in dom g & x11 = x22 ) )end;

hence
x11 = x22
; :: thesis: verumper cases
( x22 in (dom f) \ (dom g) or x22 in dom g )
by A8, XBOOLE_0:def 3;

end;

case A16:
x22 in (dom f) \ (dom g)
; :: thesis: contradiction

then
not x22 in dom g
by XBOOLE_0:def 5;

then A17: (f +* g) . x22 = f . x22 by A7, FUNCT_4:def 1;

g . x11 <> f . x22 by A3, A15, A16;

hence contradiction by A6, A9, A15, A17, FUNCT_4:def 1; :: thesis: verum

end;then A17: (f +* g) . x22 = f . x22 by A7, FUNCT_4:def 1;

g . x11 <> f . x22 by A3, A15, A16;

hence contradiction by A6, A9, A15, A17, FUNCT_4:def 1; :: thesis: verum