let f, g be Function; :: thesis: for a being set st f is one-to-one & g is one-to-one & (dom f) /\ (dom g) = {a} & (rng f) /\ (rng g) = {(f . a)} & f . a = g . a holds
(f +* g) " = (f ") +* (g ")
let a be set ; :: thesis: ( f is one-to-one & g is one-to-one & (dom f) /\ (dom g) = {a} & (rng f) /\ (rng g) = {(f . a)} & f . a = g . a implies (f +* g) " = (f ") +* (g ") )
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: (dom f) /\ (dom g) = {a} and
A4: (rng f) /\ (rng g) = {(f . a)} and
A5: f . a = g . a ; :: thesis: (f +* g) " = (f ") +* (g ")
A6: dom (g ") = rng g by A2, FUNCT_1:33;
A7: dom (f ") = rng f by A1, FUNCT_1:33;
for x being object st x in (dom (f ")) /\ (dom (g ")) holds
(f ") . x = (g ") . x

proof

let x be object ; :: thesis: ( x in (dom (f ")) /\ (dom (g ")) implies (f ") . x = (g ") . x )
{a} c= dom f by A3, XBOOLE_1:17;
then A8: a in dom f by ZFMISC_1:31;
assume A9: x in (dom (f ")) /\ (dom (g ")) ; :: thesis: (f ") . x = (g ") . x
then x = f . a by A4, A7, A6, TARSKI:def 1;
then A10: a = (f ") . x by A1, A8, FUNCT_1:32;
{a} c= dom g by A3, XBOOLE_1:17;
then A11: a in dom g by ZFMISC_1:31;
x = g . a by A4, A5, A7, A6, A9, TARSKI:def 1;
hence (f ") . x = (g ") . x by A2, A11, A10, FUNCT_1:32; :: thesis: verum

end;

then A12: f " tolerates g " ;
set gf = (f ") +* (g ");
set F = f +* g;
for x being object st x in (dom f) /\ (dom g) holds
f . x = g . x

proof

let x be object ; :: thesis: ( x in (dom f) /\ (dom g) implies f . x = g . x )
assume x in (dom f) /\ (dom g) ; :: thesis: f . x = g . x
then x = a by A3, TARSKI:def 1;
hence f . x = g . x by A5; :: thesis: verum

end;

then A13: f tolerates g ;
dom ((f ") +* (g ")) = (dom (f ")) \/ (dom (g ")) by FUNCT_4:def 1
.= (rng f) \/ (dom (g ")) by A1, FUNCT_1:33
.= (rng f) \/ (rng g) by A2, FUNCT_1:33 ;
then A14: dom ((f ") +* (g ")) = rng (f +* g) by A13, FRECHET:35;
A15: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
then A16: dom f c= dom (f +* g) by XBOOLE_1:7;
A17: dom g c= dom (f +* g) by A15, XBOOLE_1:7;
A18: rng (f +* g) = (rng f) \/ (rng g) by A13, FRECHET:35;
A19: for y, x being object holds
( y in rng (f +* g) & x = ((f ") +* (g ")) . y iff ( x in dom (f +* g) & y = (f +* g) . x ) )

proof

let y, x be object ; :: thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y iff ( x in dom (f +* g) & y = (f +* g) . x ) )

hereby :: thesis: ( x in dom (f +* g) & y = (f +* g) . x implies ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) )

assume that
A20: y in rng (f +* g) and
A21: x = ((f ") +* (g ")) . y ; :: thesis: ( x in dom (f +* g) & y = (f +* g) . x )

per cases ( y in dom (f ") or y in dom (g ") ) by A14, A20, FUNCT_4:12;

suppose A22: y in dom (f ") ; :: thesis: ( x in dom (f +* g) & y = (f +* g) . x )

then A23: y in rng f by A1, FUNCT_1:33;
A24: x = (f ") . y by A12, A21, A22, FUNCT_4:15;
then A25: y = f . x by A1, A23, FUNCT_1:32;
x in dom f by A1, A23, A24, FUNCT_1:32;
hence ( x in dom (f +* g) & y = (f +* g) . x ) by A13, A16, A25, FUNCT_4:15; :: thesis: verum

end;

suppose A26: y in dom (g ") ; :: thesis: ( x in dom (f +* g) & y = (f +* g) . x )

then A27: x = (g ") . y by A21, FUNCT_4:13;
A28: y in rng g by A2, A26, FUNCT_1:33;
then A29: y = g . x by A2, A27, FUNCT_1:32;
x in dom g by A2, A28, A27, FUNCT_1:32;
hence ( x in dom (f +* g) & y = (f +* g) . x ) by A17, A29, FUNCT_4:13; :: thesis: verum

end;

end;

end;

assume that
A30: x in dom (f +* g) and
A31: y = (f +* g) . x ; :: thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y )

per cases ( x in dom f or x in dom g ) by A30, FUNCT_4:12;

suppose A32: x in dom f ; :: thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y )

then A33: y = f . x by A13, A31, FUNCT_4:15;
then A34: x = (f ") . y by A1, A32, FUNCT_1:32;
rng (f +* g) = (rng f) \/ (rng g) by A13, FRECHET:35;
then A35: rng f c= rng (f +* g) by XBOOLE_1:7;
A36: y in rng f by A32, A33, FUNCT_1:3;
then y in dom (f ") by A1, FUNCT_1:33;
hence ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) by A12, A34, A36, A35, FUNCT_4:15; :: thesis: verum

end;

suppose A37: x in dom g ; :: thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y )

then A38: y = g . x by A31, FUNCT_4:13;
then A39: x = (g ") . y by A2, A37, FUNCT_1:32;
A40: rng g c= rng (f +* g) by A18, XBOOLE_1:7;
A41: y in rng g by A37, A38, FUNCT_1:3;
then y in dom (g ") by A2, FUNCT_1:33;
hence ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) by A39, A41, A40, FUNCT_4:13; :: thesis: verum

end;

end;

end;

f +* g is one-to-one by A1, A2, A3, A4, Th1;
hence (f +* g) " = (f ") +* (g ") by A14, A19, FUNCT_1:32; :: thesis: verum