let f be Function; :: thesis: for a being set st a in dom f holds
f | {a} = a .--> (f . a)
let a be set ; :: thesis: ( a in dom f implies f | {a} = a .--> (f . a) )
assume a in dom f ; :: thesis: f | {a} = a .--> (f . a)
hence f | {a} = {[a,(f . a)]} by GRFUNC_1:28
.= a .--> (f . a) by ZFMISC_1:29 ;
:: thesis: verum