let R be non degenerated Ring; :: thesis: for X being non empty set holds rng (IotaMap (X,R)) is linearly-independent
let X be non empty set ; :: thesis: rng (IotaMap (X,R)) is linearly-independent
set V = Free_LMod (X,R);
set A = rng (IotaMap (X,R));
for l being Linear_Combination of rng (IotaMap (X,R)) st Sum l = 0. (Free_LMod (X,R)) holds
Carrier l = {}

proof

let l be Linear_Combination of rng (IotaMap (X,R)); :: thesis: ( Sum l = 0. (Free_LMod (X,R)) implies Carrier l = {} )
assume A1: Sum l = 0. (Free_LMod (X,R)) ; :: thesis: Carrier l = {}
assume Carrier l <> {} ; :: thesis: contradiction
then consider y being object such that
A3: y in Carrier l by XBOOLE_0:def 1;
reconsider v0 = y as Element of (Free_LMod (X,R)) by A3;
A4: Carrier l c= rng (IotaMap (X,R)) by VECTSP_6:def 4;
consider x0 being object such that
A5: ( x0 in dom (IotaMap (X,R)) & (IotaMap (X,R)) . x0 = v0 ) by A3, A4, FUNCT_1:def 3;
reconsider x = x0 as Element of X by A5;
consider F being FinSequence of the carrier of (Free_LMod (X,R)) such that
A6: F is one-to-one and
A7: rng F = Carrier l and
A8: Sum l = Sum (l (#) F) by VECTSP_6:def 6;
set s = l (#) F;
set h = ev_ (x,R);
A9: rng (l (#) F) c= dom (ev_ (x,R))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (l (#) F) or y in dom (ev_ (x,R)) )
assume y in rng (l (#) F) ; :: thesis: y in dom (ev_ (x,R))
then consider t being object such that
A11: ( t in dom (l (#) F) & (l (#) F) . t = y ) by FUNCT_1:def 3;
y in the carrier of (Free_LMod (X,R)) by A11, FINSEQ_2:11;
hence y in dom (ev_ (x,R)) by FUNCT_2:def 1; :: thesis: verum

end;

len (l (#) F) = len F by VECTSP_6:def 5;
then A12: dom (l (#) F) = dom F by FINSEQ_3:29;
A13: ev_ (x,R) is additive by Th8;
A14: (ev_ (x,R)) . (Sum (l (#) F)) = 0. R by Th9, A8, A1;
consider k being object such that
A15: ( k in dom F & F . k = v0 ) by A3, A7, FUNCT_1:def 3;
len (l (#) F) = len F by VECTSP_6:def 5;
then A16: dom (l (#) F) = Seg (len F) by FINSEQ_1:def 3
.= dom F by FINSEQ_1:def 3 ;
A17: v0 = Iota (x,R) by A5, Def19;
A18: F /. k = v0 by A15, PARTFUN1:def 6;
A19: ((ev_ (x,R)) * (l (#) F)) . k = (ev_ (x,R)) . ((l (#) F) . k) by A15, A16, FUNCT_1:13
.= (ev_ (x,R)) . ((l . (F /. k)) * (F /. k)) by A15, A16, VECTSP_6:def 5
.= (l . v0) * ((ev_ (x,R)) . v0) by A18, Lm22
.= (l . v0) * (1. R) by Lm20, A17
.= l . v0 ;
A20: for i being Nat st i in dom ((ev_ (x,R)) * (l (#) F)) & i <> k holds
((ev_ (x,R)) * (l (#) F)) . i = 0. R

proof

let i be Nat; :: thesis: ( i in dom ((ev_ (x,R)) * (l (#) F)) & i <> k implies ((ev_ (x,R)) * (l (#) F)) . i = 0. R )
assume that
A21: i in dom ((ev_ (x,R)) * (l (#) F)) and
A22: i <> k ; :: thesis: ((ev_ (x,R)) * (l (#) F)) . i = 0. R
A23: i in dom F by A21, A9, RELAT_1:27, A12;
then reconsider w = F . i as Element of (Free_LMod (X,R)) by FINSEQ_2:11;
w in Carrier l by A7, A23, FUNCT_1:3;
then consider z being object such that
A25: ( z in dom (IotaMap (X,R)) & (IotaMap (X,R)) . z = w ) by A4, FUNCT_1:def 3;
reconsider x1 = z as Element of X by A25;
A26: x1 <> x by A5, A6, A23, A15, A22, A25;
w = Iota (x1,R) by A25, Def19;
then A27: (ev_ (x,R)) . w = 0. R by A26, Lm21;
len ((ev_ (x,R)) * (l (#) F)) = len (l (#) F) by FINSEQ_2:33;
then i in dom (l (#) F) by A21, FINSEQ_3:29;
then ((ev_ (x,R)) * (l (#) F)) . i = (ev_ (x,R)) . ((l (#) F) . i) by FUNCT_1:13
.= (ev_ (x,R)) . ((l . w) * w) by A23, VECTSP_6:8
.= (l . w) * ((ev_ (x,R)) . w) by Lm22
.= 0. R by A27 ;
hence ((ev_ (x,R)) * (l (#) F)) . i = 0. R ; :: thesis: verum

end;

A30: k in dom ((ev_ (x,R)) * (l (#) F)) by A15, A16, A9, RELAT_1:27;
then A31: Sum ((ev_ (x,R)) * (l (#) F)) = ((ev_ (x,R)) * (l (#) F)) /. k by A20, Lm45
.= ((ev_ (x,R)) * (l (#) F)) . k by A30, PARTFUN1:def 6 ;
l . v0 <> 0. R by A3, VECTSP_6:2;
hence contradiction by A13, Th26, A14, A19, A31; :: thesis: verum

end;

hence rng (IotaMap (X,R)) is linearly-independent ; :: thesis: verum