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 S1[ 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: S1[ 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 ; :: thesis: verum
end;
P2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume AS1: S1[n] ; :: thesis: S1[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 ;
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 ;
then P4: dom F0 = Seg n by FINSEQ_1:def 3;
A9: len F = (len F0) + 1 by ;
A11: F0 = F | (dom F0) by ;
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 ;
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 ;
then P4F: dom Fv0 = Seg n by FINSEQ_1:def 3;
A9F: len Fv = (len Fv0) + 1 by ;
P3F: Fv0 = Fv | (dom Fv0) by ;
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 ;
then dom Fv0 c= dom Fv by ;
then X1: Fv . i = <;(F /. i),v;> by ;
i in dom F0 by ;
then F /. i = F0 /. i by PARTFUN1:80;
hence Fv0 . i = <;(F0 /. i),v;> by ; :: thesis: verum
end;
reconsider i1 = Sum F0 as Element of L ;
X3: F /. (n + 1) = af by ;
thus <;(Sum F),v;> = <;(i1 + af),v;> by
.= <;i1,v;> + <;af,v;> by ZMODLAT1:def 3
.= (Sum Fv0) + <;af,v;> by P1, P1F, AS1, X0
.= (Sum Fv0) + afv by
.= Sum Fv by ; :: thesis: verum
end;
for n being Nat holds S1[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