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
ex k being Nat st
( x = (canFS (Support (@ f))) . k & k in dom (canFS (Support (@ f))) & (ev_ ((F_idxseq f),x)) . k = (@ 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
ex k being Nat st
( x = (canFS (Support (@ f))) . k & k in dom (canFS (Support (@ f))) & (ev_ ((F_idxseq f),x)) . k = (@ f) . x )
let f be Element of (Free_LMod (X,R)); :: thesis: for x being Element of X st x in Support (@ f) holds
ex k being Nat st
( x = (canFS (Support (@ f))) . k & k in dom (canFS (Support (@ f))) & (ev_ ((F_idxseq f),x)) . k = (@ f) . x )
let x be Element of X; :: thesis: ( x in Support (@ f) implies ex k being Nat st
( x = (canFS (Support (@ f))) . k & k in dom (canFS (Support (@ f))) & (ev_ ((F_idxseq f),x)) . k = (@ f) . x ) )
assume A1: x in Support (@ f) ; :: thesis: ex k being Nat st
( x = (canFS (Support (@ f))) . k & k in dom (canFS (Support (@ f))) & (ev_ ((F_idxseq f),x)) . k = (@ 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: (ev_ ((F_idxseq f),x)) . n1 = (@ f) . x

proof

reconsider i = n1 as Nat ;
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: 1. R = (@ u) . x 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 A7: (@ v) . x = ((LMULT (X,R)) . (r,u)) . x by A6, FUNCT_1:49
.= r * ((@ u) . x) by Def7
.= r by A5 ;
(ev_ ((F_idxseq f),x)) . i = (ev_ (x,R)) . ((F_idxseq f) /. i) by A3, A2, Def23
.= (ev_ (x,R)) . ((F_idxseq f) . i) by A3, A2, PARTFUN1:def 6
.= (ev_ (x,R)) . v by A3, A2, Def24
.= r by A7, Def20
.= (@ f) . x by Def20 ;
hence (ev_ ((F_idxseq f),x)) . n1 = (@ f) . x ; :: thesis: verum

end;

take n1 ; :: thesis: ( x = (canFS (Support (@ f))) . n1 & n1 in dom (canFS (Support (@ f))) & (ev_ ((F_idxseq f),x)) . n1 = (@ f) . x )
thus ( x = (canFS (Support (@ f))) . n1 & n1 in dom (canFS (Support (@ f))) & (ev_ ((F_idxseq f),x)) . n1 = (@ f) . x ) by A4, A2; :: thesis: verum