let X be non empty set ; :: thesis: for R being non degenerated Ring
for N0 being Nat
for F being FinSequence of the carrier of (Free_LMod (X,R))
for x being Element of X st len F = N0 + 1 holds
ev_ (F,x) = (ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>
let R be non degenerated Ring; :: thesis: for N0 being Nat
for F being FinSequence of the carrier of (Free_LMod (X,R))
for x being Element of X st len F = N0 + 1 holds
ev_ (F,x) = (ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>
let N0 be Nat; :: thesis: for F being FinSequence of the carrier of (Free_LMod (X,R))
for x being Element of X st len F = N0 + 1 holds
ev_ (F,x) = (ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>
let F be FinSequence of the carrier of (Free_LMod (X,R)); :: thesis: for x being Element of X st len F = N0 + 1 holds
ev_ (F,x) = (ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>
let x be Element of X; :: thesis: ( len F = N0 + 1 implies ev_ (F,x) = (ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*> )
assume A1: len F = N0 + 1 ; :: thesis: ev_ (F,x) = (ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>
then A2: dom F = Seg (N0 + 1) by FINSEQ_1:def 3;
then A3: Seg (N0 + 1) = dom (ev_ (F,x)) by Def23
.= Seg (len (ev_ (F,x))) by FINSEQ_1:def 3 ;
A4: N0 + 1 = len ((F | N0) ^ <*(F /. (len F))*>) by A1, FINSEQ_5:21
.= (len (F | N0)) + 1 by FINSEQ_2:16 ;
A5: Seg (len (ev_ ((F | N0),x))) = dom (ev_ ((F | N0),x)) by FINSEQ_1:def 3
.= dom (F | N0) by Def23
.= Seg N0 by A4, FINSEQ_1:def 3 ;
then A6: len (ev_ ((F | N0),x)) = N0 by FINSEQ_1:6;
len <*((ev_ (x,R)) . (F /. (len F)))*> = 1 by FINSEQ_1:39;
then A7: len ((ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>) = N0 + 1 by A6, FINSEQ_1:22;
for k being Nat st 1 <= k & k <= len (ev_ (F,x)) holds
(ev_ (F,x)) . k = ((ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (ev_ (F,x)) implies (ev_ (F,x)) . k = ((ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>) . k )
assume ( 1 <= k & k <= len (ev_ (F,x)) ) ; :: thesis: (ev_ (F,x)) . k = ((ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>) . k
then A8: k in Seg (N0 + 1) by A3;
then A9: k in (Seg N0) \/ {(N0 + 1)} by FINSEQ_1:9;
A10: Seg N0 c= Seg (N0 + 1) by FINSEQ_3:18;

per cases ( k in Seg N0 or k in {(N0 + 1)} ) by A9, XBOOLE_0:def 3;

suppose A11: k in Seg N0 ; :: thesis: (ev_ (F,x)) . k = ((ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>) . k

then A12: k in dom (F | N0) by A4, FINSEQ_1:def 3;
then A13: k in dom (ev_ ((F | N0),x)) by Def23;
A14: k in dom (F | (Seg N0)) by A11, A4, FINSEQ_1:def 3;
A15: (F | N0) /. k = (F | (Seg N0)) . k by A12, PARTFUN1:def 6
.= F . k by A14, FUNCT_1:47
.= F /. k by A2, A11, A10, PARTFUN1:def 6 ;
((ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (N0 + 1)))*>) . k = (ev_ ((F | N0),x)) . k by A13, FINSEQ_1:def 7
.= (ev_ (x,R)) . (F /. k) by A15, A12, Def23
.= (ev_ (F,x)) . k by Def23, A8, A2 ;
hence (ev_ (F,x)) . k = ((ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>) . k by A1; :: thesis: verum

end;

suppose k in {(N0 + 1)} ; :: thesis: (ev_ (F,x)) . k = ((ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>) . k

then A16: k = N0 + 1 by TARSKI:def 1;
N0 + 1 = (len (ev_ ((F | N0),x))) + 1 by A5, FINSEQ_1:6;
hence (ev_ (F,x)) . k = ((ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*>) . k by A1, Def23, A2, FINSEQ_1:4, A16; :: thesis: verum

end;

end;

end;

hence ev_ (F,x) = (ev_ ((F | N0),x)) ^ <*((ev_ (x,R)) . (F /. (len F)))*> by A3, A7, FINSEQ_1:6; :: thesis: verum