let R be non degenerated Ring; :: thesis: for X being non empty set
for z being Element of X holds Support (iota (z,R)) = {z}
let X be non empty set ; :: thesis: for z being Element of X holds Support (iota (z,R)) = {z}
let z be Element of X; :: thesis: Support (iota (z,R)) = {z}
thus Support (iota (z,R)) c= {z} :: according to XBOOLE_0:def 10 :: thesis: {z} c= Support (iota (z,R))

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in Support (iota (z,R)) or o in {z} )
assume A2: o in Support (iota (z,R)) ; :: thesis: o in {z}
then A3: (iota (z,R)) . o <> 0. R by POLYNOM1:def 3;
assume not o in {z} ; :: thesis: contradiction
then A5: o <> z by TARSKI:def 1;
o in dom (iota (z,R)) by A2, POLYNOM1:def 3;
hence contradiction by A3, A5, Def17; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in {z} or o in Support (iota (z,R)) )
assume A7: o in {z} ; :: thesis: o in Support (iota (z,R))
then A8: o = z by TARSKI:def 1;
A9: dom (iota (z,R)) = X by FUNCT_2:def 1;
(iota (z,R)) . o = 1. R by A8, Def17;
then (iota (z,R)) . o <> 0. R ;
hence o in Support (iota (z,R)) by A7, A9, POLYNOM1:def 3; :: thesis: verum