let X be set ; :: thesis: for f, g being Function holds (f | X) +* g = (f | (X \ (dom g))) \/ g
let f, g be Function; :: thesis: (f | X) +* g = (f | (X \ (dom g))) \/ g
set f1 = f | (X \ (dom g));
set a1 = g;
( dom (f | (X \ (dom g))) c= X \ (dom g) & X \ (dom g) misses dom g ) by XBOOLE_1:79;
then A1: f | (X \ (dom g)) tolerates g by PARTFUN1:56, XBOOLE_1:63;
(f | X) +* g = (f | ((X \ (dom g)) \/ (X /\ (dom g)))) +* g by Th48
.= ((f | (X \ (dom g))) +* (f | (X /\ (dom g)))) +* g by FUNCT_4:78
.= (f | (X \ (dom g))) +* ((f | (X /\ (dom g))) +* ((g null {}) null ({} \/ (dom g)))) by FUNCT_4:14
.= (f | (X \ (dom g))) +* (((f | X) | (dom g)) +* (g | (dom g))) by RELAT_1:71
.= (f | (X \ (dom g))) +* (((f | X) +* g) | (dom g)) by FUNCT_4:71
.= (f | (X \ (dom g))) +* g
.= (f | (X \ (dom g))) \/ g by A1, FUNCT_4:30 ;
hence (f | X) +* g = (f | (X \ (dom g))) \/ g ; :: thesis: verum