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_{1}[ 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_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[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

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

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

proof

P2:
for n being Nat st S
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;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

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume AS1: S_{1}[n]
; :: thesis: S_{1}[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;>

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;assume AS1: S

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

reconsider i1 = Sum F0 as Element of L ;
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;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

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

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