let X be non empty set ; :: thesis: for R being non degenerated Ring
for x being Element of X
for r being Element of R st r <> 0. R holds
Support (@ (r * (Iota (x,R)))) = {x}
let R be non degenerated Ring; :: thesis: for x being Element of X
for r being Element of R st r <> 0. R holds
Support (@ (r * (Iota (x,R)))) = {x}
let x be Element of X; :: thesis: for r being Element of R st r <> 0. R holds
Support (@ (r * (Iota (x,R)))) = {x}
let r be Element of R; :: thesis: ( r <> 0. R implies Support (@ (r * (Iota (x,R)))) = {x} )
assume A1: r <> 0. R ; :: thesis: Support (@ (r * (Iota (x,R)))) = {x}
thus Support (@ (r * (Iota (x,R)))) c= {x} :: according to XBOOLE_0:def 10 :: thesis: {x} c= Support (@ (r * (Iota (x,R))))

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in Support (@ (r * (Iota (x,R)))) or o in {x} )
assume A2: o in Support (@ (r * (Iota (x,R)))) ; :: thesis: o in {x}
then reconsider x1 = o as Element of X ;
A3: (@ (r * (Iota (x,R)))) . x1 = r * ((@ (Iota (x,R))) . x1) by Th7;

per cases ( o = x or o <> x ) ;

suppose o = x ; :: thesis: o in {x}

hence o in {x} by TARSKI:def 1; :: thesis: verum

end;

suppose o <> x ; :: thesis: o in {x}

then (@ (Iota (x,R))) . o = 0. R by A2, Def17;
hence o in {x} by A2, A3, POLYNOM1:def 4; :: thesis: verum

end;

end;

end;

(@ (Iota (x,R))) . x = 1. R by Def17;
then (@ (r * (Iota (x,R)))) . x = r * (1. R) by Th7
.= r ;
then x in Support (@ (r * (Iota (x,R)))) by A1, POLYNOM1:def 4;
hence {x} c= Support (@ (r * (Iota (x,R)))) by ZFMISC_1:31; :: thesis: verum