let R be non degenerated Ring; :: thesis: for X being non empty set
for x, y being Element of X st x <> y holds
(ev_ (x,R)) . (iota (y,R)) = 0. R
let X be non empty set ; :: thesis: for x, y being Element of X st x <> y holds
(ev_ (x,R)) . (iota (y,R)) = 0. R
let x, y be Element of X; :: thesis: ( x <> y implies (ev_ (x,R)) . (iota (y,R)) = 0. R )
assume A1: x <> y ; :: thesis: (ev_ (x,R)) . (iota (y,R)) = 0. R
(ev_ (x,R)) . (iota (y,R)) = (@ (Iota (y,R))) . x by Def20
.= 0. R by Def17, A1 ;
hence (ev_ (x,R)) . (iota (y,R)) = 0. R ; :: thesis: verum