let X be non empty set ; :: thesis: for R being non degenerated Ring
for f being Element of (Free_LMod (X,R)) holds Support (ev_iota f) = Support (@ f)
let R be non degenerated Ring; :: thesis: for f being Element of (Free_LMod (X,R)) holds Support (ev_iota f) = Support (@ f)
let f be Element of (Free_LMod (X,R)); :: thesis: Support (ev_iota f) = Support (@ f)
thus Support (ev_iota f) c= Support (@ f) :: according to XBOOLE_0:def 10 :: thesis: Support (@ f) c= Support (ev_iota f)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in Support (ev_iota f) or o in Support (@ f) )
assume A2: o in Support (ev_iota f) ; :: thesis: o in Support (@ f)
then reconsider x = o as Element of X ;
assume A3: not o in Support (@ f) ; :: thesis: contradiction
reconsider gx = (IotaMap (X,R)) . x as Element of (Free_LMod (X,R)) ;
(ev_iota f) . x = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x) by Def21
.= ((@ f) . x) * gx by Def20
.= (0. R) * gx by A3, POLYNOM1:def 4
.= 0. (Free_LMod (X,R)) by VECTSP_1:14 ;
hence contradiction by A2, POLYNOM1:def 4; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in Support (@ f) or o in Support (ev_iota f) )
assume A4: o in Support (@ f) ; :: thesis: o in Support (ev_iota f)
then reconsider x = o as Element of X ;
reconsider r = (ev_ (x,R)) . f as Element of the carrier of R ;
reconsider u = Iota (x,R) as Element of (Free_LMod (X,R)) ;
reconsider v = (ev_iota f) . x as Element of (Free_LMod (X,R)) ;
A5: (@ u) . x = 1. R by Def17;
A6: [r,u] in [: the carrier of R,(fs_Funcs (X,R)):] ;
v = ((ev_ (x,R)) . f) * ((IotaMap (X,R)) . x) by Def21
.= (fs_LMULT (X,R)) . (r,u) by Def19 ;
then (@ v) . x = ((LMULT (X,R)) . (r,u)) . x by A6, FUNCT_1:49
.= r * ((@ u) . x) by Def7
.= r by A5 ;
then @ v <> 0. (Free_LMod (X,R)) by A4, Lm18;
hence o in Support (ev_iota f) by POLYNOM1:def 4; :: thesis: verum