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 x in Support (@ f) holds
(@ f) . x = (@ (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 x in Support (@ f) holds
(@ f) . x = (@ (Sum (F_idxseq f))) . x
let f be Element of (Free_LMod (X,R)); :: thesis: for x being Element of X st x in Support (@ f) holds
(@ f) . x = (@ (Sum (F_idxseq f))) . x
let x be Element of X; :: thesis: ( x in Support (@ f) implies (@ f) . x = (@ (Sum (F_idxseq f))) . x )
assume A1: x in Support (@ f) ; :: thesis: (@ f) . x = (@ (Sum (F_idxseq f))) . x
rng (canFS (Support (@ f))) = Support (@ f) by FUNCT_2:def 3;
then consider o being object such that
A2: ( o in dom (canFS (Support (@ f))) & x = (canFS (Support (@ f))) . o ) by A1, FUNCT_1:def 3;
reconsider n1 = o as Nat by A2;
A3: 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 ;
A4: dom (ev_ ((F_idxseq f),x)) = dom (F_idxseq f) by Def23;
A5: n1 in dom (ev_ ((F_idxseq f),x)) by A3, A2, Def23;
A6: for i being Nat st i in dom (ev_ ((F_idxseq f),x)) & i <> n1 holds
(ev_ ((F_idxseq f),x)) . i = 0. R

proof

let i be Nat; :: thesis: ( i in dom (ev_ ((F_idxseq f),x)) & i <> n1 implies (ev_ ((F_idxseq f),x)) . i = 0. R )
assume A7: ( i in dom (ev_ ((F_idxseq f),x)) & i <> n1 ) ; :: thesis: (ev_ ((F_idxseq f),x)) . i = 0. R
then A8: i in dom (F_idxseq f) by Def23;
A9: i in dom (idxseq f) by A3, Def23, A7;
then (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 A2, A7, A9, FUNCT_1:def 4;
then A10: 0. R = (@ u) . x by Def17;
A11: [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 A12: (@ v) . x = ((LMULT (X,R)) . (r,u)) . x by A11, FUNCT_1:49
.= r * ((@ u) . x) by Def7
.= 0. R by A10 ;
(ev_ ((F_idxseq f),x)) . i = (ev_ (x,R)) . ((F_idxseq f) /. i) by A4, A7, Def23
.= (ev_ (x,R)) . ((F_idxseq f) . i) by A8, PARTFUN1:def 6
.= (ev_ (x,R)) . ((ev_iota f) . ((idxseq f) . i)) by A8, Def24
.= 0. R by Def20, A12 ;
hence (ev_ ((F_idxseq f),x)) . i = 0. R ; :: thesis: verum

end;

consider k being Nat such that
A13: ( x = (canFS (Support (@ f))) . k & k in dom (canFS (Support (@ f))) & (ev_ ((F_idxseq f),x)) . k = (@ f) . x ) by A1, Th13;
A14: (ev_ ((F_idxseq f),x)) . n1 = (@ f) . x by A2, A13, FUNCT_1:def 4;
Sum (ev_ ((F_idxseq f),x)) = (ev_ (x,R)) . (Sum (F_idxseq f)) by Th11
.= (@ (Sum (F_idxseq f))) . x by Def20 ;
hence (@ f) . x = (@ (Sum (F_idxseq f))) . x by A14, A5, A6, MATRIX_3:12; :: thesis: verum