let f be Function; :: thesis: for x being set holds f +~ x,x = f
let x be set ; :: thesis: f +~ x,x = f
A: (id {x}) * f c= f by RELAT_1:76;
thus f +~ x,x = f +* ((id {x}) * f) by Th102
.= f by A, Th104 ; :: thesis: verum