let X be non empty set ; :: thesis: for R being non degenerated Ring
for f being Element of (Free_LMod (X,R))
for x being Element of X holds
( x in Support (@ f) iff (ev_ (x,R)) . f <> 0. R )
let R be non degenerated Ring; :: thesis: for f being Element of (Free_LMod (X,R))
for x being Element of X holds
( x in Support (@ f) iff (ev_ (x,R)) . f <> 0. R )
let f be Element of (Free_LMod (X,R)); :: thesis: for x being Element of X holds
( x in Support (@ f) iff (ev_ (x,R)) . f <> 0. R )
let x be Element of X; :: thesis: ( x in Support (@ f) iff (ev_ (x,R)) . f <> 0. R )
A1: ( x in Support (@ f) implies (ev_ (x,R)) . f <> 0. R )

proof

assume A2: x in Support (@ f) ; :: thesis: (ev_ (x,R)) . f <> 0. R
(ev_ (x,R)) . f = (@ f) . x by Def20;
hence (ev_ (x,R)) . f <> 0. R by A2, POLYNOM1:def 4; :: thesis: verum

end;

( (ev_ (x,R)) . f <> 0. R implies x in Support (@ f) )

proof

assume A3: (ev_ (x,R)) . f <> 0. R ; :: thesis: x in Support (@ f)
(ev_ (x,R)) . f = (@ f) . x by Def20;
hence x in Support (@ f) by A3, POLYNOM1:def 4; :: thesis: verum

end;

hence ( x in Support (@ f) iff (ev_ (x,R)) . f <> 0. R ) by A1; :: thesis: verum