let f be Function; :: thesis: for x being set st x in dom f holds
f +* (x .--> (f . x)) = f
let x be set ; :: thesis: ( x in dom f implies f +* (x .--> (f . x)) = f )
assume x in dom f ; :: thesis: f +* (x .--> (f . x)) = f
hence f +* (x .--> (f . x)) = f +* x,(f . x) by Def3
.= f by Th37 ;
:: thesis: verum