let X, a be set ; :: thesis: for f being Function st dom f = X \/ {a} holds
f = (f | X) +* (a .--> (f . a))
let f be Function; :: thesis: ( dom f = X \/ {a} implies f = (f | X) +* (a .--> (f . a)) )
assume A1: dom f = X \/ {a} ; :: thesis: f = (f | X) +* (a .--> (f . a))
a in {a} by TARSKI:def 1;
then A2: a in dom f by A1, XBOOLE_0:def 3;
thus f = (f | X) +* (f | {a}) by A1, FUNCT_4:70
.= (f | X) +* (a .--> (f . a)) by A2, Th6 ; :: thesis: verum