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 Def2
.= f by Th34 ;
:: thesis: verum