let f be Function; :: thesis: for x being set st x in dom f holds
f | {x} = {[x,(f . x)]}
let x be set ; :: thesis: ( x in dom f implies f | {x} = {[x,(f . x)]} )
assume A1: x in dom f ; :: thesis: f | {x} = {[x,(f . x)]}
A2: x in {x} by TARSKI:def 1;
dom (f | {x}) = (dom f) /\ {x} by RELAT_1:61
.= {x} by A1, ZFMISC_1:46 ;
hence f | {x} = {[x,((f | {x}) . x)]} by Th7
.= {[x,(f . x)]} by A2, FUNCT_1:49 ;
:: thesis: verum