let f be Function; :: thesis: for x, y being set st not x in dom f holds
f c= f +* (x .--> y)
let x, y be set ; :: thesis: ( not x in dom f implies f c= f +* (x .--> y) )
assume not x in dom f ; :: thesis: f c= f +* (x .--> y)
then dom f misses {x} by ZFMISC_1:56;
then dom f misses dom (x .--> y) by FUNCOP_1:19;
hence f c= f +* (x .--> y) by Th33; :: thesis: verum