let f, g be Function; for B, C being set st dom f c= B & dom g c= C & B misses C holds
( (f +* g) | B = f & (f +* g) | C = g )
let B, C be set ; ( dom f c= B & dom g c= C & B misses C implies ( (f +* g) | B = f & (f +* g) | C = g ) )
assume that
A1:
dom f c= B
and
A2:
dom g c= C
and
A3:
B misses C
; ( (f +* g) | B = f & (f +* g) | C = g )
dom f misses C
by A1, A3, XBOOLE_1:63;
then
(dom f) /\ C = {}
by XBOOLE_0:def 7;
then
dom (f | C) = {}
by RELAT_1:90;
then A4:
f | C = {}
;
dom g misses B
by A2, A3, XBOOLE_1:63;
then
(dom g) /\ B = {}
by XBOOLE_0:def 7;
then
dom (g | B) = {}
by RELAT_1:90;
then A5:
g | B = {}
;
thus (f +* g) | B =
(f | B) +* (g | B)
by Th75
.=
f | B
by A5, Th22
.=
f
by A1, RELAT_1:97
; (f +* g) | C = g
thus (f +* g) | C =
(f | C) +* (g | C)
by Th75
.=
g | C
by A4, Th21
.=
g
by A2, RELAT_1:97
; verum