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:55;
A7: dom (f " ) = rng f by A1, FUNCT_1:55;
for x being set st x in (dom (f " )) /\ (dom (g " )) holds
(f " ) . x = (g " ) . x

proof

let x be set ; :: 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:37;
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:54;
{a} c= dom g by A3, XBOOLE_1:17;
then A11: a in dom g by ZFMISC_1:37;
x = g . a by A4, A5, A7, A6, A9, TARSKI:def 1;
hence (f " ) . x = (g " ) . x by A2, A11, A10, FUNCT_1:54; :: thesis: verum

end;

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

proof

let x be set ; :: 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 by PARTFUN1:def 6;
dom ((f " ) +* (g " )) = (dom (f " )) \/ (dom (g " )) by FUNCT_4:def 1
.= (rng f) \/ (dom (g " )) by A1, FUNCT_1:55
.= (rng f) \/ (rng g) by A2, FUNCT_1:55 ;
then A14: dom ((f " ) +* (g " )) = rng (f +* g) by A13, FRECHET:39;
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:39;
A19: for y, x being set 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 set ; :: 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:13;

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:55;
A24: x = (f " ) . y by A12, A21, A22, FUNCT_4:16;
then A25: y = f . x by A1, A23, FUNCT_1:54;
x in dom f by A1, A23, A24, FUNCT_1:54;
hence ( x in dom (f +* g) & y = (f +* g) . x ) by A13, A16, A25, FUNCT_4:16; :: 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:14;
A28: y in rng g by A2, A26, FUNCT_1:55;
then A29: y = g . x by A2, A27, FUNCT_1:54;
x in dom g by A2, A28, A27, FUNCT_1:54;
hence ( x in dom (f +* g) & y = (f +* g) . x ) by A17, A29, FUNCT_4:14; :: 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:13;

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:16;
then A34: x = (f " ) . y by A1, A32, FUNCT_1:54;
rng (f +* g) = (rng f) \/ (rng g) by A13, FRECHET:39;
then A35: rng f c= rng (f +* g) by XBOOLE_1:7;
A36: y in rng f by A32, A33, FUNCT_1:12;
then y in dom (f " ) by A1, FUNCT_1:55;
hence ( y in rng (f +* g) & x = ((f " ) +* (g " )) . y ) by A12, A34, A36, A35, FUNCT_4:16; :: 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:14;
then A39: x = (g " ) . y by A2, A37, FUNCT_1:54;
A40: rng g c= rng (f +* g) by A18, XBOOLE_1:7;
A41: y in rng g by A37, A38, FUNCT_1:12;
then y in dom (g " ) by A2, FUNCT_1:55;
hence ( y in rng (f +* g) & x = ((f " ) +* (g " )) . y ) by A39, A41, A40, FUNCT_4:14; :: thesis: verum

end;

end;

end;

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