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 st not x in Support (@ f) holds
0. R = (@ (Sum (F_idxseq f))) . x
let R be non degenerated Ring; :: thesis: for f being Element of (Free_LMod (X,R))
for x being Element of X st not x in Support (@ f) holds
0. R = (@ (Sum (F_idxseq f))) . x
let f be Element of (Free_LMod (X,R)); :: thesis: for x being Element of X st not x in Support (@ f) holds
0. R = (@ (Sum (F_idxseq f))) . x
let x be Element of X; :: thesis: ( not x in Support (@ f) implies 0. R = (@ (Sum (F_idxseq f))) . x )
assume A1: not x in Support (@ f) ; :: thesis: 0. R = (@ (Sum (F_idxseq f))) . x
A2: dom (F_idxseq f) = Seg (len (F_idxseq f)) by FINSEQ_1:def 3
.= Seg (len (idxseq f)) by Def24
.= dom (idxseq f) by FINSEQ_1:def 3 ;
A3: dom (ev_ ((F_idxseq f),x)) = dom (F_idxseq f) by Def23;
A4: for i being Nat st i in dom (ev_ ((F_idxseq f),x)) holds
(ev_ ((F_idxseq f),x)) . i = 0. R

proof

let i be Nat; :: thesis: ( i in dom (ev_ ((F_idxseq f),x)) implies (ev_ ((F_idxseq f),x)) . i = 0. R )
assume A5: i in dom (ev_ ((F_idxseq f),x)) ; :: thesis: (ev_ ((F_idxseq f),x)) . i = 0. R
then A6: i in dom (F_idxseq f) by Def23;
i in dom (idxseq f) by A2, Def23, A5;
then A8: (canFS (Support (@ f))) . i in rng (canFS (Support (@ f))) by FUNCT_1:3;
then (canFS (Support (@ f))) . i in Support (@ f) ;
then reconsider x1 = (canFS (Support (@ f))) . i as Element of X ;
reconsider r = (ev_ (x1,R)) . f as Element of the carrier of R ;
reconsider u = Iota (x1,R) as Element of (Free_LMod (X,R)) ;
reconsider v = (ev_iota f) . x1 as Element of (Free_LMod (X,R)) ;
x <> x1 by A1, A8;
then A9: 0. R = (@ u) . x by Def17;
A10: [r,u] in [: the carrier of R,(fs_Funcs (X,R)):] ;
v = ((ev_ (x1,R)) . f) * ((IotaMap (X,R)) . x1) by Def21
.= (fs_LMULT (X,R)) . (r,u) by Def19 ;
then A11: (@ v) . x = ((LMULT (X,R)) . (r,u)) . x by A10, FUNCT_1:49
.= r * ((@ u) . x) by Def7
.= 0. R by A9 ;
(ev_ ((F_idxseq f),x)) . i = (ev_ (x,R)) . ((F_idxseq f) /. i) by A3, A5, Def23
.= (ev_ (x,R)) . ((F_idxseq f) . i) by A6, PARTFUN1:def 6
.= (ev_ (x,R)) . ((ev_iota f) . ((idxseq f) . i)) by A6, Def24
.= 0. R by A11, Def20 ;
hence (ev_ ((F_idxseq f),x)) . i = 0. R ; :: thesis: verum

end;

reconsider p = ev_ ((F_idxseq f),x) as FinSequence of R ;
for k being Element of NAT st k in dom p holds
p . k = 0. R by A4;
then 0. R = Sum (ev_ ((F_idxseq f),x)) by MATRIX_3:35
.= (ev_ (x,R)) . (Sum (F_idxseq f)) by Th11
.= (@ (Sum (F_idxseq f))) . x by Def20 ;
hence 0. R = (@ (Sum (F_idxseq f))) . x ; :: thesis: verum