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 )
set fg = f +* g;
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: rng f misses rng g ; :: thesis: f +* g is one-to-one
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: 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 that
A4: x1 in dom (f +* g) and
A5: x2 in dom (f +* g) and
A6: (f +* g) . x1 = (f +* g) . x2 ; :: thesis: x1 = x2
A7: ( x1 in dom f or x1 in dom g ) by A4, Th12;
A8: ( x2 in dom f or x2 in dom g ) by A5, Th12;
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 A9: ( x1 in dom g & x2 in dom g ) ; :: thesis: x1 = x2
then ( (f +* g) . x1 = g . x1 & (f +* g) . x2 = g . x2 ) by Th13;
hence x1 = x2 by A2, A6, A9; :: thesis: verum
end;
suppose A10: ( x1 in dom g & not x2 in dom g ) ; :: thesis: x1 = x2
then x2 in dom f by A5, Th12;
then A11: f . x2 in rng f by FUNCT_1:def 3;
A12: g . x1 in rng g by A10, FUNCT_1:def 3;
( (f +* g) . x1 = g . x1 & (f +* g) . x2 = f . x2 ) by A10, Th11, Th13;
hence x1 = x2 by A3, A6, A12, A11, XBOOLE_0:3; :: thesis: verum
end;
suppose A13: ( not x1 in dom g & x2 in dom g ) ; :: thesis: x1 = x2
then x1 in dom f by A4, Th12;
then A14: f . x1 in rng f by FUNCT_1:def 3;
A15: g . x2 in rng g by A13, FUNCT_1:def 3;
( (f +* g) . x1 = f . x1 & (f +* g) . x2 = g . x2 ) by A13, Th11, Th13;
hence x1 = x2 by A3, A6, A15, A14, XBOOLE_0:3; :: thesis: verum
end;
suppose A16: ( 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 Th11;
hence x1 = x2 by A1, A6, A7, A8, A16; :: thesis: verum
end;
end;