let f be Function; :: thesis: f +* {} = f
A1: 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;

(dom f) \/ (dom {}) = dom f ;
then dom (f +* {}) = dom f by Def1;
hence f +* {} = f by A1, FUNCT_1:2; :: thesis: verum