let f, g be Function; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( (f +* g) | B = f & (f +* g) | C = g )
dom f misses C by A1, A3, XBOOLE_1:63;
then (dom f) /\ C = {} ;
then dom (f | C) = {} by RELAT_1:61;
then A4: f | C = {} ;
dom g misses B by A2, A3, XBOOLE_1:63;
then (dom g) /\ B = {} ;
then dom (g | B) = {} by RELAT_1:61;
then A5: g | B = {} ;
thus (f +* g) | B = (f | B) +* (g | B) by Th71
.= f | B by A5
.= f by A1, RELAT_1:68 ; :: thesis: (f +* g) | C = g
thus (f +* g) | C = (f | C) +* (g | C) by Th71
.= g | C by A4
.= g by A2, RELAT_1:68 ; :: thesis: verum