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 " )
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 A6: f tolerates g by PARTFUN1:def 6;
A7: ( dom (f " ) = rng f & dom (g " ) = rng g ) by A1, A2, 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 )
assume A8: x in (dom (f " )) /\ (dom (g " )) ; :: thesis: (f " ) . x = (g " ) . x
{a} c= dom f by A3, XBOOLE_1:17;
then A9: a in dom f by ZFMISC_1:37;
{a} c= dom g by A3, XBOOLE_1:17;
then A10: a in dom g by ZFMISC_1:37;
x = f . a by A4, A7, A8, TARSKI:def 1;
then A11: a = (f " ) . x by A1, A9, FUNCT_1:54;
x = g . a by A4, A5, A7, A8, TARSKI:def 1;
hence (f " ) . x = (g " ) . x by A2, A10, A11, FUNCT_1:54; :: thesis: verum

end;

then A12: f " tolerates g " by PARTFUN1:def 6;
A13: f +* g is one-to-one by A1, A2, A3, A4, Th5;
A14: rng (f +* g) = (rng f) \/ (rng g) by A6, FRECHET:39;
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 A15: dom ((f " ) +* (g " )) = rng (f +* g) by A6, FRECHET:39;
A16: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
then A17: dom f c= dom (f +* g) by XBOOLE_1:7;
A18: dom g c= dom (f +* g) by A16, XBOOLE_1:7;
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 A19: ( y in rng (f +* g) & 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 A15, A19, FUNCT_4:13;

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

then A21: y in rng f by A1, FUNCT_1:55;
x = (f " ) . y by A12, A19, A20, FUNCT_4:16;
then ( x in dom f & y = f . x ) by A1, A21, FUNCT_1:54;
hence ( x in dom (f +* g) & y = (f +* g) . x ) by A6, A17, FUNCT_4:16; :: thesis: verum

end;

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

then A23: y in rng g by A2, FUNCT_1:55;
x = (g " ) . y by A19, A22, FUNCT_4:14;
then ( x in dom g & y = g . x ) by A2, A23, FUNCT_1:54;
hence ( x in dom (f +* g) & y = (f +* g) . x ) by A18, FUNCT_4:14; :: thesis: verum

end;

end;

end;

assume A24: ( x in dom (f +* g) & 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 A24, FUNCT_4:13;

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

then A26: y = f . x by A6, A24, FUNCT_4:16;
then A27: x = (f " ) . y by A1, A25, FUNCT_1:54;
A28: y in rng f by A25, A26, FUNCT_1:12;
rng (f +* g) = (rng f) \/ (rng g) by A6, FRECHET:39;
then A29: rng f c= rng (f +* g) by XBOOLE_1:7;
y in dom (f " ) by A1, A28, FUNCT_1:55;
hence ( y in rng (f +* g) & x = ((f " ) +* (g " )) . y ) by A12, A27, A28, A29, FUNCT_4:16; :: thesis: verum

end;

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

then A31: y = g . x by A24, FUNCT_4:14;
then A32: x = (g " ) . y by A2, A30, FUNCT_1:54;
A33: y in rng g by A30, A31, FUNCT_1:12;
A34: rng g c= rng (f +* g) by A14, XBOOLE_1:7;
y in dom (g " ) by A2, A33, FUNCT_1:55;
hence ( y in rng (f +* g) & x = ((f " ) +* (g " )) . y ) by A32, A33, A34, FUNCT_4:14; :: thesis: verum

end;

end;

end;

hence (f +* g) " = (f " ) +* (g " ) by A13, A15, FUNCT_1:54; :: thesis: verum