let X be non empty set ; :: thesis: for R being non degenerated Ring
for F being FinSequence of the carrier of (Free_LMod (X,R))
for x being Element of X holds (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x))
let R be non degenerated Ring; :: thesis: for F being FinSequence of the carrier of (Free_LMod (X,R))
for x being Element of X holds (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x))
let F be FinSequence of the carrier of (Free_LMod (X,R)); :: thesis: for x being Element of X holds (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x))
let x be Element of X; :: thesis: (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x))

per cases ( len F = 0 or len F <> 0 ) ;

suppose A1: len F = 0 ; :: thesis: (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x))

then F = <*> the carrier of (Free_LMod (X,R)) ;
then Sum F = 0. (Free_LMod (X,R)) by RLVECT_1:43;
then A2: (ev_ (x,R)) . (Sum F) = 0. R by Th9;
Seg (len F) = dom F by FINSEQ_1:def 3
.= dom (ev_ (F,x)) by Def23
.= Seg (len (ev_ (F,x))) by FINSEQ_1:def 3 ;
then ev_ (F,x) = <*> the carrier of R by A1;
hence (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x)) by A2, RLVECT_1:43; :: thesis: verum

end;

suppose A3: len F <> 0 ; :: thesis: (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x))

for k being non zero Nat st len F = k holds
(ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x))

proof

let k be non zero Nat; :: thesis: ( len F = k implies (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x)) )
defpred S₁[ non zero Nat] means for F being FinSequence of the carrier of (Free_LMod (X,R)) st len F = $1 holds
(ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x));
A4: S₁[1]

proof

for F being FinSequence of the carrier of (Free_LMod (X,R)) st len F = 1 holds
(ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x))

proof

let F be FinSequence of the carrier of (Free_LMod (X,R)); :: thesis: ( len F = 1 implies (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x)) )
assume A5: len F = 1 ; :: thesis: (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x))
then dom F = Seg 1 by FINSEQ_1:def 3;
then A6: 1 in dom F ;
then F . 1 in rng F by FUNCT_1:3;
then reconsider o = F . 1 as Element of (Free_LMod (X,R)) ;
F = <*o*> by A5, FINSEQ_1:40;
then A7: Sum F = F . 1 by RLVECT_1:44
.= F /. 1 by A6, PARTFUN1:def 6 ;
set o1 = (ev_ (F,x)) . 1;
set o = (ev_ (F,x)) /. 1;
A8: dom (ev_ (F,x)) = dom F by Def23
.= Seg 1 by A5, FINSEQ_1:def 3 ;
then A9: 1 in dom (ev_ (F,x)) ;
A10: dom (ev_ (F,x)) = dom F by Def23;
ev_ (F,x) = <*((ev_ (F,x)) . 1)*> by A8, FINSEQ_1:def 8
.= <*((ev_ (F,x)) /. 1)*> by A9, PARTFUN1:def 6 ;
then Sum (ev_ (F,x)) = (ev_ (F,x)) . 1 by BINOM:3
.= (ev_ (x,R)) . (Sum F) by A7, A9, A10, Def23 ;
hence (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x)) ; :: thesis: verum

end;

hence S₁[1] ; :: thesis: verum

end;

A11: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A12: S₁[k] ; :: thesis: S₁[k + 1]
for F being FinSequence of the carrier of (Free_LMod (X,R)) st len F = k + 1 holds
(ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x))

proof

let F be FinSequence of the carrier of (Free_LMod (X,R)); :: thesis: ( len F = k + 1 implies (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x)) )
assume A13: len F = k + 1 ; :: thesis: (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x))
then consider G being FinSequence of (Free_LMod (X,R)), d being Element of (Free_LMod (X,R)) such that
A14: F = G ^ <*d*> by FINSEQ_2:19;
(F | k) ^ <*(F /. (len F))*> = G ^ <*d*> by A14, A13, FINSEQ_5:21;
then A15: ( G = F | k & d = F /. (len F) ) by FINSEQ_2:17;
A16: k + 1 = (len G) + 1 by FINSEQ_2:16, A14, A13;
Sum F = (Sum G) + d by A14, FVSUM_1:71;
then (ev_ (x,R)) . (Sum F) = ((ev_ (x,R)) . (Sum G)) + ((ev_ (x,R)) . d) by Th8
.= (Sum (ev_ ((F | k),x))) + ((ev_ (x,R)) . (F /. (len F))) by A16, A12, A15
.= Sum ((ev_ ((F | k),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>) by FVSUM_1:71
.= Sum (ev_ (F,x)) by A13, Th10 ;
hence (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x)) ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A4, A11);
hence ( len F = k implies (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x)) ) ; :: thesis: verum

end;

hence (ev_ (x,R)) . (Sum F) = Sum (ev_ (F,x)) by A3; :: thesis: verum

end;

end;