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:50 ; :: thesis: verum