for r being Element of R holds r in (singleton R) . r

proof

hence
singleton R is map-reflexive
; :: thesis: verum
let r be Element of R; :: thesis: r in (singleton R) . r

r in {r} by TARSKI:def 1;

hence r in (singleton R) . r by SingleFunc; :: thesis: verum

end;r in {r} by TARSKI:def 1;

hence r in (singleton R) . r by SingleFunc; :: thesis: verum