let R be non degenerated Ring; :: thesis: for X being non empty set
for f being Element of (Free_LMod (X,R)) holds f in Lin (rng (IotaMap (X,R)))
let X be non empty set ; :: thesis: for f being Element of (Free_LMod (X,R)) holds f in Lin (rng (IotaMap (X,R)))
let f be Element of (Free_LMod (X,R)); :: thesis: f in Lin (rng (IotaMap (X,R)))
set s = F_idxseq f;
set W = Lin (rng (IotaMap (X,R)));
A1: for i being Nat st i in dom (F_idxseq f) holds
(F_idxseq f) /. i in Lin (rng (IotaMap (X,R))) by Lm42;
Sum (F_idxseq f) in Lin (rng (IotaMap (X,R)))

proof

defpred S₁[ Nat] means for t being FinSequence of the carrier of (Free_LMod (X,R)) st len t = $1 & ( for j being Nat st j in dom t holds
t /. j in Lin (rng (IotaMap (X,R))) ) holds
Sum t in Lin (rng (IotaMap (X,R)));
A3: S₁[ 0 ]

proof

let t be FinSequence of the carrier of (Free_LMod (X,R)); :: thesis: ( len t = 0 & ( for j being Nat st j in dom t holds
t /. j in Lin (rng (IotaMap (X,R))) ) implies Sum t in Lin (rng (IotaMap (X,R))) )
assume that
A4: len t = 0 and
for j being Nat st j in dom t holds
t /. j in Lin (rng (IotaMap (X,R))) ; :: thesis: Sum t in Lin (rng (IotaMap (X,R)))
Sum t = 0. (Free_LMod (X,R)) by A4, RLVECT_1:75;
hence Sum t in Lin (rng (IotaMap (X,R))) by VECTSP_4:17; :: thesis: verum

end;

A5: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
let t be FinSequence of the carrier of (Free_LMod (X,R)); :: thesis: ( len t = n + 1 & ( for j being Nat st j in dom t holds
t /. j in Lin (rng (IotaMap (X,R))) ) implies Sum t in Lin (rng (IotaMap (X,R))) )
assume that
A7: len t = n + 1 and
A8: for j being Nat st j in dom t holds
t /. j in Lin (rng (IotaMap (X,R))) ; :: thesis: Sum t in Lin (rng (IotaMap (X,R)))
set g0 = t | (Seg n);
A9: t | (Seg n) is FinSequence by FINSEQ_1:15;
A10: rng (t | (Seg n)) c= the carrier of (Free_LMod (X,R)) ;
reconsider g = t | (Seg n) as FinSequence of the carrier of (Free_LMod (X,R)) by A9, A10, FINSEQ_1:def 4;
A11: n <= len t by A7, NAT_1:11;
then A12: len g = n by FINSEQ_1:17;
A13: for j being Nat st j in dom g holds
g /. j in Lin (rng (IotaMap (X,R)))

proof

let j be Nat; :: thesis: ( j in dom g implies g /. j in Lin (rng (IotaMap (X,R))) )
assume A14: j in dom g ; :: thesis: g /. j in Lin (rng (IotaMap (X,R)))
then A15: j in Seg n by FINSEQ_1:17, A11;
Seg n c= Seg (n + 1) by NAT_1:11, FINSEQ_1:5;
then j in Seg (n + 1) by A15;
then A16: j in dom t by A7, FINSEQ_1:def 3;
g /. j = g . j by A14, PARTFUN1:def 6
.= t . j by A15, FUNCT_1:49
.= t /. j by A16, PARTFUN1:def 6 ;
hence g /. j in Lin (rng (IotaMap (X,R))) by A16, A8; :: thesis: verum

end;

A17: Sum g in Lin (rng (IotaMap (X,R))) by A6, A12, A13;
n + 1 in Seg (len t) by A7, FINSEQ_1:4;
then A18: n + 1 in dom t by FINSEQ_1:def 3;
then t /. (n + 1) in Lin (rng (IotaMap (X,R))) by A8;
then A20: t . (n + 1) in Lin (rng (IotaMap (X,R))) by A18, PARTFUN1:def 6;
Seg (n + 1) = dom t by A7, FINSEQ_1:def 3;
then A21: t = t | (Seg (n + 1)) ;
t . (n + 1) in rng t by FUNCT_1:3, A18;
then reconsider tn = t . (n + 1) as Element of (Free_LMod (X,R)) ;
t = g ^ <*(t . (n + 1))*> by A18, FINSEQ_5:10, A21;
then Sum t = (Sum g) + tn by FVSUM_1:71;
hence Sum t in Lin (rng (IotaMap (X,R))) by A17, A20, VECTSP_4:20; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A5);
then S₁[ len (F_idxseq f)] ;
hence Sum (F_idxseq f) in Lin (rng (IotaMap (X,R))) by A1; :: thesis: verum

end;

hence f in Lin (rng (IotaMap (X,R))) by Th15; :: thesis: verum