let X be non empty set ; :: thesis: for R being non degenerated Ring
for f being Element of (Free_LMod (X,R))
for i being Nat st i in dom (idxseq f) holds
Support (@ ((F_idxseq f) /. i)) = {((idxseq f) . i)}
let R be non degenerated Ring; :: thesis: for f being Element of (Free_LMod (X,R))
for i being Nat st i in dom (idxseq f) holds
Support (@ ((F_idxseq f) /. i)) = {((idxseq f) . i)}
let f be Element of (Free_LMod (X,R)); :: thesis: for i being Nat st i in dom (idxseq f) holds
Support (@ ((F_idxseq f) /. i)) = {((idxseq f) . i)}
let i be Nat; :: thesis: ( i in dom (idxseq f) implies Support (@ ((F_idxseq f) /. i)) = {((idxseq f) . i)} )
assume A1: i in dom (idxseq f) ; :: thesis: Support (@ ((F_idxseq f) /. i)) = {((idxseq f) . i)}
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 ;
reconsider x9 = (idxseq f) . i as Element of X by A1, FINSEQ_2:11;
rng (canFS (Support (@ f))) = Support (@ f) by FUNCT_2:def 3;
then x9 in Support (@ f) by A1, FUNCT_1:3;
then (@ f) . x9 <> 0. R by POLYNOM1:def 4;
then A6: (ev_ (x9,R)) . f <> 0. R by Def20;
reconsider r = (ev_ (x9,R)) . f as Element of the carrier of R ;
(F_idxseq f) /. i = (F_idxseq f) . i by A1, A2, PARTFUN1:def 6
.= (ev_iota f) . x9 by A1, A2, Def24
.= ((ev_ (x9,R)) . f) * ((IotaMap (X,R)) . x9) by Def21
.= r * (Iota (x9,R)) by Def19 ;
hence Support (@ ((F_idxseq f) /. i)) = {((idxseq f) . i)} by A6, Lm23; :: thesis: verum