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