let f, g be Function; :: thesis: (f +* g) | ((dom f) \ (dom g)) c= f
A1: for x being object st x in dom ((f +* g) | ((dom f) \ (dom g))) holds
((f +* g) | ((dom f) \ (dom g))) . x = f . x

proof

let x be object ; :: thesis: ( x in dom ((f +* g) | ((dom f) \ (dom g))) implies ((f +* g) | ((dom f) \ (dom g))) . x = f . x )
assume A2: x in dom ((f +* g) | ((dom f) \ (dom g))) ; :: thesis: ((f +* g) | ((dom f) \ (dom g))) . x = f . x
dom ((f +* g) | ((dom f) \ (dom g))) c= (dom f) \ (dom g) by RELAT_1:58;
then not x in dom g by A2, XBOOLE_0:def 5;
then (f +* g) . x = f . x by Th11;
hence ((f +* g) | ((dom f) \ (dom g))) . x = f . x by A2, FUNCT_1:47; :: thesis: verum

end;

dom ((f +* g) | ((dom f) \ (dom g))) c= (dom f) \ (dom g) by RELAT_1:58;
then dom ((f +* g) | ((dom f) \ (dom g))) c= dom f by XBOOLE_1:1;
hence (f +* g) | ((dom f) \ (dom g)) c= f by A1, GRFUNC_1:2; :: thesis: verum