let f be Function; :: thesis: for x, y being object st not x in dom f holds
f c= f +* (x .--> y)
let x, y be object ; :: 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:50;
then dom f misses dom (x .--> y) ;
hence f c= f +* (x .--> y) by Th32; :: thesis: verum