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 ) )

.= (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

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

dom ((f ") +* (g ")) =
(dom (f ")) \/ (dom (g "))
by FUNCT_4:def 1
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 ) )

end;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

thus
( x in dom (f +* g) & y = (f +* g) . x implies ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) )
:: thesis: verum
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 )

end;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;

end;

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;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

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;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

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 )

end;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;

end;

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;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

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;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

.= (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