let f be Function; :: thesis: for x being object holds f +~ (x,x) = f
let x be object ; :: thesis: f +~ (x,x) = f
thus f +~ (x,x) = f +* ((id {x}) * f) by Th96
.= f by Th98, RELAT_1:50 ; :: thesis: verum