let f, g be Function; :: thesis: ( f is one-to-one & g is one-to-one & rng f misses rng g implies f +* g is one-to-one )
assume A1: ( f is one-to-one & g is one-to-one & rng f misses rng g ) ; :: thesis: f +* g is one-to-one
set fg = f +* g;
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom (f +* g) or not x2 in dom (f +* g) or not (f +* g) . x1 = (f +* g) . x2 or x1 = x2 )
assume A2: ( x1 in dom (f +* g) & x2 in dom (f +* g) & (f +* g) . x1 = (f +* g) . x2 ) ; :: thesis: x1 = x2
then A3: ( ( x1 in dom f or x1 in dom g ) & ( x2 in dom f or x2 in dom g ) ) by Th13;

per cases ( ( x1 in dom g & x2 in dom g ) or ( x1 in dom g & not x2 in dom g ) or ( not x1 in dom g & x2 in dom g ) or ( not x1 in dom g & not x2 in dom g ) ) ;

suppose A4: ( x1 in dom g & x2 in dom g ) ; :: thesis: x1 = x2

then ( (f +* g) . x1 = g . x1 & (f +* g) . x2 = g . x2 ) by Th14;
hence x1 = x2 by A1, A2, A4, FUNCT_1:def 8; :: thesis: verum

end;

suppose A5: ( x1 in dom g & not x2 in dom g ) ; :: thesis: x1 = x2

then A6: x2 in dom f by A2, Th13;
A7: ( (f +* g) . x1 = g . x1 & (f +* g) . x2 = f . x2 ) by A5, Th12, Th14;
( g . x1 in rng g & f . x2 in rng f ) by A5, A6, FUNCT_1:def 5;
hence x1 = x2 by A1, A2, A7, XBOOLE_0:3; :: thesis: verum

end;

suppose A8: ( not x1 in dom g & x2 in dom g ) ; :: thesis: x1 = x2

then A9: x1 in dom f by A2, Th13;
A10: ( (f +* g) . x1 = f . x1 & (f +* g) . x2 = g . x2 ) by A8, Th12, Th14;
( g . x2 in rng g & f . x1 in rng f ) by A8, A9, FUNCT_1:def 5;
hence x1 = x2 by A1, A2, A10, XBOOLE_0:3; :: thesis: verum

end;

suppose A11: ( not x1 in dom g & not x2 in dom g ) ; :: thesis: x1 = x2

then ( (f +* g) . x1 = f . x1 & (f +* g) . x2 = f . x2 ) by Th12;
hence x1 = x2 by A1, A2, A3, A11, FUNCT_1:def 8; :: thesis: verum

end;

end;