let f, g be one-to-one Function; :: thesis: ( dom f misses dom g & rng f misses rng g implies (f +* g) " = (f ") +* (g ") )
assume that
A1: dom f misses dom g and
A2: rng f misses rng g ; :: thesis: (f +* g) " = (f ") +* (g ")
A3: f +* g is one-to-one by A2, FUNCT_4:92;
A4: 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 ) )
thus ( y in rng (f +* g) & x = ((f ") +* (g ")) . y implies ( x in dom (f +* g) & y = (f +* g) . x ) ) :: thesis: ( x in dom (f +* g) & y = (f +* g) . x implies ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) )

proof

A5: rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
assume that
A6: y in rng (f +* g) and
A7: x = ((f ") +* (g ")) . y ; :: thesis: ( x in dom (f +* g) & y = (f +* g) . x )

per cases ( y in rng f or y in rng g ) by A6, A5, XBOOLE_0:def 3;

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

then consider z being object such that
A9: z in dom f and
A10: y = f . z by FUNCT_1:def 3;
dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
then A11: z in dom (f +* g) by A9, XBOOLE_0:def 3;
A12: ( dom (f ") = rng f & dom (g ") = rng g ) by FUNCT_1:33;
( y = (f +* g) . z & z = (f ") . y ) by A1, A9, A10, FUNCT_1:32, FUNCT_4:16;
hence ( x in dom (f +* g) & y = (f +* g) . x ) by A2, A7, A8, A11, A12, FUNCT_4:16; :: thesis: verum

end;

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

A14: ( dom (f ") = rng f & dom (g ") = rng g ) by FUNCT_1:33;
consider z being object such that
A15: z in dom g and
A16: y = g . z by A13, FUNCT_1:def 3;
z = (g ") . y by A15, A16, FUNCT_1:32;
then z = ((g ") +* (f ")) . y by A2, A13, A14, FUNCT_4:16;
then A17: z = x by A2, A7, A14, FUNCT_4:35;
( dom (f +* g) = (dom f) \/ (dom g) & y = (g +* f) . z ) by A1, A15, A16, FUNCT_4:16, FUNCT_4:def 1;
hence ( x in dom (f +* g) & y = (f +* g) . x ) by A1, A15, A17, FUNCT_4:35, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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

proof

A18: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
assume that
A19: x in dom (f +* g) and
A20: 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 A19, A18, XBOOLE_0:def 3;

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

then not x in dom g by A1, XBOOLE_0:3;
then A22: y = f . x by A20, FUNCT_4:11;
then A23: x = (f ") . y by A21, FUNCT_1:32;
A24: ( dom (f ") = rng f & dom (g ") = rng g ) by FUNCT_1:33;
A25: y in rng f by A21, A22, FUNCT_1:def 3;
then y in (rng f) \/ (rng g) by XBOOLE_0:def 3;
hence ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) by A1, A2, A25, A23, A24, FRECHET:35, FUNCT_4:16, PARTFUN1:56; :: thesis: verum

end;

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

then A27: y = g . x by A20, FUNCT_4:13;
then A28: y in rng g by A26, FUNCT_1:def 3;
then A29: y in (rng f) \/ (rng g) by XBOOLE_0:def 3;
A30: ( dom (f ") = rng f & dom (g ") = rng g ) by FUNCT_1:33;
x = (g ") . y by A26, A27, FUNCT_1:32;
then x = ((g ") +* (f ")) . y by A2, A28, A30, FUNCT_4:16;
hence ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) by A1, A2, A29, A30, FRECHET:35, FUNCT_4:35, PARTFUN1:56; :: thesis: verum

end;

end;

end;

end;

dom ((f ") +* (g ")) = (dom (f ")) \/ (dom (g ")) by FUNCT_4:def 1
.= (rng f) \/ (dom (g ")) by FUNCT_1:33
.= (rng f) \/ (rng g) by FUNCT_1:33
.= rng (f +* g) by A1, FRECHET:35, PARTFUN1:56 ;
hence (f +* g) " = (f ") +* (g ") by A3, A4, FUNCT_1:32; :: thesis: verum