let f, g be Function; ( dom f misses dom g & rng g misses dom f implies for X being set holds f * (X -indexing g) = f | X )
assume that
A1:
dom f misses dom g
and
A2:
rng g misses dom f
; for X being set holds f * (X -indexing g) = f | X
let X be set ; f * (X -indexing g) = f | X
A3:
dom (f | X) c= dom f
by RELAT_1:60;
A4:
(id X) .: (dom (g | X)) c= dom (g | X)
dom (g | X) c= dom g
by RELAT_1:60;
then
dom (f | X) misses dom (g | X)
by A1, A3, XBOOLE_1:64;
then A5:
(id X) .: (dom (g | X)) misses dom (f | X)
by A4, XBOOLE_1:64;
A6:
dom (f | X) c= X
by RELAT_1:58;
rng (g | X) c= rng g
by RELAT_1:70;
then A7:
dom (f | X) misses rng (g | X)
by A2, A3, XBOOLE_1:64;
g .: X c= rng g
by RELAT_1:111;
then
g .: X misses dom f
by A2, XBOOLE_1:64;
then A8:
(g .: X) /\ (dom f) = {}
;
rng (X -indexing g) = (X \ (dom g)) \/ (g .: X)
by Th7;
then (rng (X -indexing g)) /\ (dom f) =
((X \ (dom g)) /\ (dom f)) \/ ((g .: X) /\ (dom f))
by XBOOLE_1:23
.=
(X \ (dom g)) /\ (dom f)
by A8
;
then
(rng (X -indexing g)) /\ (dom f) c= X /\ (dom f)
by XBOOLE_1:26;
then
(rng (X -indexing g)) /\ (dom f) c= dom (f | X)
by RELAT_1:61;
hence f * (X -indexing g) =
(f | X) * ((id X) +* (g | X))
by Th2, RELAT_1:59
.=
(f | X) * (id X)
by A7, A5, Th3
.=
f | X
by A6, RELAT_1:51
;
verum