let L be non trivial positive-definite RATional Z_Lattice; :: thesis: for v being Element of L
for b being FinSequence of L
for sbv being FinSequence of F_Rat st len b = len sbv & ( for n being Nat st n in dom sbv holds
sbv . n = <;(b /. n),v;> ) holds
<;(Sum b),v;> = Sum sbv
let v be Element of L; :: thesis: for b being FinSequence of L
for sbv being FinSequence of F_Rat st len b = len sbv & ( for n being Nat st n in dom sbv holds
sbv . n = <;(b /. n),v;> ) holds
<;(Sum b),v;> = Sum sbv
defpred S₁[ Nat] means for F being FinSequence of L
for Fv being FinSequence of F_Rat st len F = $1 & len F = len Fv & ( for i being Nat st i in dom Fv holds
Fv . i = <;(F /. i),v;> ) holds
<;(Sum F),v;> = Sum Fv;
P1: S₁[ 0 ]

proof

let F be FinSequence of L; :: thesis: for Fv being FinSequence of F_Rat st len F = 0 & len F = len Fv & ( for i being Nat st i in dom Fv holds
Fv . i = <;(F /. i),v;> ) holds
<;(Sum F),v;> = Sum Fv
let Fv be FinSequence of F_Rat; :: thesis: ( len F = 0 & len F = len Fv & ( for i being Nat st i in dom Fv holds
Fv . i = <;(F /. i),v;> ) implies <;(Sum F),v;> = Sum Fv )
assume AS1: ( len F = 0 & len F = len Fv & ( for i being Nat st i in dom Fv holds
Fv . i = <;(F /. i),v;> ) ) ; :: thesis: <;(Sum F),v;> = Sum Fv
F = <*> the carrier of L by AS1;
then Sum F = 0. L by RLVECT_1:43;
then X1: <;(Sum F),v;> = 0. F_Rat by ZMODLAT1:12;
Fv = <*> the carrier of F_Rat by AS1;
hence <;(Sum F),v;> = Sum Fv by X1, RLVECT_1:43; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume AS1: S₁[n] ; :: thesis: S₁[n + 1]
let F be FinSequence of L; :: thesis: for Fv being FinSequence of F_Rat st len F = n + 1 & len F = len Fv & ( for i being Nat st i in dom Fv holds
Fv . i = <;(F /. i),v;> ) holds
<;(Sum F),v;> = Sum Fv
let Fv be FinSequence of F_Rat; :: thesis: ( len F = n + 1 & len F = len Fv & ( for i being Nat st i in dom Fv holds
Fv . i = <;(F /. i),v;> ) implies <;(Sum F),v;> = Sum Fv )
assume AS2: ( len F = n + 1 & len F = len Fv & ( for i being Nat st i in dom Fv holds
Fv . i = <;(F /. i),v;> ) ) ; :: thesis: <;(Sum F),v;> = Sum Fv
reconsider F0 = F | n as FinSequence of L ;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A70: n + 1 in dom F by AS2, FINSEQ_1:def 3;
then F . (n + 1) in rng F by FUNCT_1:3;
then reconsider af = F . (n + 1) as Element of L ;
P1: len F0 = n by FINSEQ_1:59, AS2, NAT_1:11;
then P4: dom F0 = Seg n by FINSEQ_1:def 3;
A9: len F = (len F0) + 1 by AS2, FINSEQ_1:59, NAT_1:11;
A11: F0 = F | (dom F0) by P1, FINSEQ_1:def 3;
reconsider Fv0 = Fv | n as FinSequence of F_Rat ;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A70F: n + 1 in dom Fv by AS2, FINSEQ_1:def 3;
then Fv . (n + 1) in rng Fv by FUNCT_1:3;
then reconsider afv = Fv . (n + 1) as Element of F_Rat ;
P1F: len Fv0 = n by FINSEQ_1:59, AS2, NAT_1:11;
then P4F: dom Fv0 = Seg n by FINSEQ_1:def 3;
A9F: len Fv = (len Fv0) + 1 by AS2, FINSEQ_1:59, NAT_1:11;
P3F: Fv0 = Fv | (dom Fv0) by P1F, FINSEQ_1:def 3;
X0: for i being Nat st i in dom Fv0 holds
Fv0 . i = <;(F0 /. i),v;>

proof

let i be Nat; :: thesis: ( i in dom Fv0 implies Fv0 . i = <;(F0 /. i),v;> )
assume P40: i in dom Fv0 ; :: thesis: Fv0 . i = <;(F0 /. i),v;>
dom Fv = Seg (n + 1) by AS2, FINSEQ_1:def 3;
then dom Fv0 c= dom Fv by P4F, FINSEQ_1:5, NAT_1:11;
then X1: Fv . i = <;(F /. i),v;> by AS2, P40;
i in dom F0 by P40, P4, P1F, FINSEQ_1:def 3;
then F /. i = F0 /. i by PARTFUN1:80;
hence Fv0 . i = <;(F0 /. i),v;> by X1, P40, FUNCT_1:47; :: thesis: verum

end;

reconsider i1 = Sum F0 as Element of L ;
X3: F /. (n + 1) = af by A70, PARTFUN1:def 6;
thus <;(Sum F),v;> = <;(i1 + af),v;> by AS2, A9, A11, RLVECT_1:38
.= <;i1,v;> + <;af,v;> by ZMODLAT1:def 3
.= (Sum Fv0) + <;af,v;> by P1, P1F, AS1, X0
.= (Sum Fv0) + afv by A70F, AS2, X3
.= Sum Fv by AS2, P3F, A9F, RLVECT_1:38 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(P1, P2);
hence for b being FinSequence of L
for sbv being FinSequence of F_Rat st len b = len sbv & ( for n being Nat st n in dom sbv holds
sbv . n = <;(b /. n),v;> ) holds
<;(Sum b),v;> = Sum sbv ; :: thesis: verum