let f be Function; :: thesis: f +* {} = f
(dom f) \/ (dom {} ) = dom f ;
then A1: dom (f +* {} ) = dom f by Def1;
for x being set st x in dom f holds
(f +* {} ) . x = f . x

proof

let x be set ; :: thesis: ( x in dom f implies (f +* {} ) . x = f . x )
assume x in dom f ; :: thesis: (f +* {} ) . x = f . x
then x in (dom f) \ (dom {} ) ;
hence (f +* {} ) . x = f . x by Th12; :: thesis: verum

end;

hence f +* {} = f by A1, FUNCT_1:9; :: thesis: verum