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: dom ((f " ) +* (g " )) = (dom (f " )) \/ (dom (g " )) by FUNCT_4:def 1
.= (rng f) \/ (dom (g " )) by FUNCT_1:55
.= (rng f) \/ (rng g) by FUNCT_1:55
.= rng (f +* g) by A1, FRECHET:39, PARTFUN1:138 ;
A4: f +* g is one-to-one by A2, FUNCT_4:98;
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 ) )
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

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

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

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

then consider z being set such that
A9: z in dom f and
A10: y = f . z by FUNCT_1:def 5;
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: y = (f +* g) . z by A1, A9, A10, FUNCT_4:17;
A13: z = (f " ) . y by A9, A10, FUNCT_1:54;
( dom (f " ) = rng f & dom (g " ) = rng g ) by FUNCT_1:55;
hence ( x in dom (f +* g) & y = (f +* g) . x ) by A2, A6, A8, A11, A12, A13, FUNCT_4:17; :: thesis: verum

end;

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

then consider z being set such that
A15: z in dom g and
A16: y = g . z by FUNCT_1:def 5;
A17: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
A18: y = (g +* f) . z by A1, A15, A16, FUNCT_4:17;
A19: z = (g " ) . y by A15, A16, FUNCT_1:54;
A20: ( dom (f " ) = rng f & dom (g " ) = rng g ) by FUNCT_1:55;
then z = ((g " ) +* (f " )) . y by A2, A14, A19, FUNCT_4:17;
then z = x by A2, A6, A20, FUNCT_4:36;
hence ( x in dom (f +* g) & y = (f +* g) . x ) by A1, A15, A17, A18, FUNCT_4:36, 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

assume that
A21: x in dom (f +* g) and
A22: y = (f +* g) . x ; :: thesis: ( y in rng (f +* g) & x = ((f " ) +* (g " )) . y )
A23: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;

per cases ( x in dom f or x in dom g ) by A21, A23, XBOOLE_0:def 3;

suppose A24: 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 A25: y = f . x by A22, FUNCT_4:12;
then A26: y in rng f by A24, FUNCT_1:def 5;
then A27: y in (rng f) \/ (rng g) by XBOOLE_0:def 3;
A28: x = (f " ) . y by A24, A25, FUNCT_1:54;
( dom (f " ) = rng f & dom (g " ) = rng g ) by FUNCT_1:55;
hence ( y in rng (f +* g) & x = ((f " ) +* (g " )) . y ) by A1, A2, A26, A27, A28, Th7, FUNCT_4:17; :: thesis: verum

end;

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

then A30: y = g . x by A22, FUNCT_4:14;
then A31: y in rng g by A29, FUNCT_1:def 5;
then A32: y in (rng f) \/ (rng g) by XBOOLE_0:def 3;
A33: x = (g " ) . y by A29, A30, FUNCT_1:54;
A34: ( dom (f " ) = rng f & dom (g " ) = rng g ) by FUNCT_1:55;
then x = ((g " ) +* (f " )) . y by A2, A31, A33, FUNCT_4:17;
hence ( y in rng (f +* g) & x = ((f " ) +* (g " )) . y ) by A1, A2, A32, A34, Th7, FUNCT_4:36; :: thesis: verum

end;

end;

end;

end;

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