let R be non degenerated Ring; :: thesis: for X being non empty set
for f being Element of (Free_LMod (X,R))
for i being Nat st i in dom (F_idxseq f) holds
(F_idxseq f) /. i in Lin (rng (IotaMap (X,R)))
let X be non empty set ; :: thesis: for f being Element of (Free_LMod (X,R))
for i being Nat st i in dom (F_idxseq f) holds
(F_idxseq f) /. i in Lin (rng (IotaMap (X,R)))
let f be Element of (Free_LMod (X,R)); :: thesis: for i being Nat st i in dom (F_idxseq f) holds
(F_idxseq f) /. i in Lin (rng (IotaMap (X,R)))
let i be Nat; :: thesis: ( i in dom (F_idxseq f) implies (F_idxseq f) /. i in Lin (rng (IotaMap (X,R))) )
assume A1: i in dom (F_idxseq f) ; :: thesis: (F_idxseq f) /. i in Lin (rng (IotaMap (X,R)))
set g = (F_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 x = (idxseq f) . i as Element of X by A1, A2, FINSEQ_2:11;
A3: Support (@ ((F_idxseq f) /. i)) = {x} by A1, A2, Lm24;
set W = Lin (rng (IotaMap (X,R)));
(IotaMap (X,R)) . x in Lin (rng (IotaMap (X,R))) by FUNCT_2:4, VECTSP_7:8;
then ((@ ((F_idxseq f) /. i)) . x) * ((IotaMap (X,R)) . x) in Lin (rng (IotaMap (X,R))) by VECTSP_4:21;
hence (F_idxseq f) /. i in Lin (rng (IotaMap (X,R))) by A3, Lm26; :: thesis: verum