let R be non degenerated Ring; :: thesis: for X being non empty set
for x being Element of X holds (ev_ (x,R)) . (iota (x,R)) = 1. R
let X be non empty set ; :: thesis: for x being Element of X holds (ev_ (x,R)) . (iota (x,R)) = 1. R
let x be Element of X; :: thesis: (ev_ (x,R)) . (iota (x,R)) = 1. R
(ev_ (x,R)) . (iota (x,R)) = (@ (Iota (x,R))) . x by Def20
.= 1. R by Def17 ;
hence (ev_ (x,R)) . (iota (x,R)) = 1. R ; :: thesis: verum