let L be non empty right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for s being FinSequence of L

for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)

let s be FinSequence of L; :: thesis: for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)

let q be Element of L; :: thesis: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) implies Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) )

assume A1: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) ) ; :: thesis: Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)

defpred S_{1}[ Nat] means for s being FinSequence of L st len s = $1 holds

for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q);

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A23, A2);

hence Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) by A1; :: thesis: verum

for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)

let s be FinSequence of L; :: thesis: for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)

let q be Element of L; :: thesis: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) implies Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) )

assume A1: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) ) ; :: thesis: Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)

defpred S

for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q);

A2: for k being Nat st S

S

proof

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A3: S

now :: thesis: for s being FinSequence of L st len s = k + 1 holds

for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)

hence
Sfor q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)

let s be FinSequence of L; :: thesis: ( len s = k + 1 implies for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) )

set f = s | (Seg k);

reconsider f = s | (Seg k) as FinSequence by FINSEQ_1:15;

assume A4: len s = k + 1 ; :: thesis: for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)

then A5: 1 <= len s by NAT_1:12;

then len s in dom s by FINSEQ_3:25;

then A6: s /. (len s) = s . (len s) by PARTFUN1:def 6;

A7: k <= len s by A4, NAT_1:13;

then A8: len f = k by FINSEQ_1:17;

then reconsider f = f as FinSequence of L by FINSEQ_1:def 4;

A13: len s = (len f) + 1 by A4, A7, FINSEQ_1:17;

let q be Element of L; :: thesis: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) implies Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) )

assume that

A14: q <> 1. L and

A15: for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ; :: thesis: Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)

then A17: (len s) -' 1 = (len s) - 1 by XREAL_0:def 2

.= ((len f) + 1) - 1 by A4, A7, FINSEQ_1:17 ;

hence Sum s = (Sum f) + (s /. (len s)) by A13, A6, RLVECT_1:38

.= (((1. L) - (q |^ (len f))) / ((1. L) - q)) + (s /. (len s)) by A3, A14, A7, A18, FINSEQ_1:17

.= (((1. L) - (q |^ (len f))) / ((1. L) - q)) + (q |^ (len f)) by A15, A5, A17, A6

.= (((1. L) - (q |^ (len f))) / ((1. L) - q)) + (((q |^ (len f)) * ((1. L) - q)) / ((1. L) - q)) by A16, Th3

.= (((1. L) - (q |^ (len f))) + ((q |^ (len f)) * ((1. L) - q))) / ((1. L) - q) by VECTSP_1:def 3

.= (((1. L) - (q |^ (len f))) + (((q |^ (len f)) * (1. L)) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by VECTSP_1:def 2

.= (((1. L) - (q |^ (len f))) + ((q |^ (len f)) + ((q |^ (len f)) * (- q)))) / ((1. L) - q)

.= ((1. L) + ((- (q |^ (len f))) + ((q |^ (len f)) + ((q |^ (len f)) * (- q))))) / ((1. L) - q) by RLVECT_1:def 3

.= ((1. L) + (((- (q |^ (len f))) + (q |^ (len f))) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by RLVECT_1:def 3

.= ((1. L) + ((0. L) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by RLVECT_1:5

.= ((1. L) + ((q |^ (len f)) * (- q))) / ((1. L) - q) by ALGSTR_1:def 2

.= ((1. L) + (- ((q |^ (len f)) * q))) / ((1. L) - q) by VECTSP_1:8

.= ((1. L) - (q |^ (len s))) / ((1. L) - q) by A13, GROUP_1:def 7 ;

:: thesis: verum

end;s . i = q |^ (i -' 1) ) holds

Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) )

set f = s | (Seg k);

reconsider f = s | (Seg k) as FinSequence by FINSEQ_1:15;

assume A4: len s = k + 1 ; :: thesis: for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)

then A5: 1 <= len s by NAT_1:12;

then len s in dom s by FINSEQ_3:25;

then A6: s /. (len s) = s . (len s) by PARTFUN1:def 6;

A7: k <= len s by A4, NAT_1:13;

then A8: len f = k by FINSEQ_1:17;

now :: thesis: for u being object st u in rng f holds

u in the carrier of L

then
rng f c= the carrier of L
by TARSKI:def 3;u in the carrier of L

let u be object ; :: thesis: ( u in rng f implies u in the carrier of L )

assume u in rng f ; :: thesis: u in the carrier of L

then consider x being object such that

A9: x in dom f and

A10: f . x = u by FUNCT_1:def 3;

reconsider x9 = x as Element of NAT by A9;

x9 <= len f by A9, FINSEQ_3:25;

then A11: x9 <= len s by A4, A8, NAT_1:12;

1 <= x9 by A9, FINSEQ_3:25;

then A12: x in dom s by A11, FINSEQ_3:25;

f . x = s . x by A9, FUNCT_1:47

.= s /. x by A12, PARTFUN1:def 6 ;

hence u in the carrier of L by A10; :: thesis: verum

end;assume u in rng f ; :: thesis: u in the carrier of L

then consider x being object such that

A9: x in dom f and

A10: f . x = u by FUNCT_1:def 3;

reconsider x9 = x as Element of NAT by A9;

x9 <= len f by A9, FINSEQ_3:25;

then A11: x9 <= len s by A4, A8, NAT_1:12;

1 <= x9 by A9, FINSEQ_3:25;

then A12: x in dom s by A11, FINSEQ_3:25;

f . x = s . x by A9, FUNCT_1:47

.= s /. x by A12, PARTFUN1:def 6 ;

hence u in the carrier of L by A10; :: thesis: verum

then reconsider f = f as FinSequence of L by FINSEQ_1:def 4;

A13: len s = (len f) + 1 by A4, A7, FINSEQ_1:17;

let q be Element of L; :: thesis: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) implies Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) )

assume that

A14: q <> 1. L and

A15: for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ; :: thesis: Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)

A16: now :: thesis: not (1. L) - q = 0. L

(len s) - 1 >= 1 - 1
by A5, XREAL_1:9;assume
(1. L) - q = 0. L
; :: thesis: contradiction

then ((1. L) - q) + q = q by ALGSTR_1:def 2;

then (1. L) + ((- q) + q) = q by RLVECT_1:def 3;

then (1. L) + (0. L) = q by RLVECT_1:5;

hence contradiction by A14, RLVECT_1:def 4; :: thesis: verum

end;then ((1. L) - q) + q = q by ALGSTR_1:def 2;

then (1. L) + ((- q) + q) = q by RLVECT_1:def 3;

then (1. L) + (0. L) = q by RLVECT_1:5;

hence contradiction by A14, RLVECT_1:def 4; :: thesis: verum

then A17: (len s) -' 1 = (len s) - 1 by XREAL_0:def 2

.= ((len f) + 1) - 1 by A4, A7, FINSEQ_1:17 ;

A18: now :: thesis: for i being Nat st 1 <= i & i <= len f holds

f . i = q |^ (i -' 1)

f = s | (dom f)
by A7, FINSEQ_1:17;f . i = q |^ (i -' 1)

let i be Nat; :: thesis: ( 1 <= i & i <= len f implies f . i = q |^ (i -' 1) )

assume that

A19: 1 <= i and

A20: i <= len f ; :: thesis: f . i = q |^ (i -' 1)

A21: i <= len s by A4, A8, A20, NAT_1:13;

i in dom f by A19, A20, FINSEQ_3:25;

hence f . i = s . i by FUNCT_1:47

.= q |^ (i -' 1) by A15, A19, A21 ;

:: thesis: verum

end;assume that

A19: 1 <= i and

A20: i <= len f ; :: thesis: f . i = q |^ (i -' 1)

A21: i <= len s by A4, A8, A20, NAT_1:13;

i in dom f by A19, A20, FINSEQ_3:25;

hence f . i = s . i by FUNCT_1:47

.= q |^ (i -' 1) by A15, A19, A21 ;

:: thesis: verum

hence Sum s = (Sum f) + (s /. (len s)) by A13, A6, RLVECT_1:38

.= (((1. L) - (q |^ (len f))) / ((1. L) - q)) + (s /. (len s)) by A3, A14, A7, A18, FINSEQ_1:17

.= (((1. L) - (q |^ (len f))) / ((1. L) - q)) + (q |^ (len f)) by A15, A5, A17, A6

.= (((1. L) - (q |^ (len f))) / ((1. L) - q)) + (((q |^ (len f)) * ((1. L) - q)) / ((1. L) - q)) by A16, Th3

.= (((1. L) - (q |^ (len f))) + ((q |^ (len f)) * ((1. L) - q))) / ((1. L) - q) by VECTSP_1:def 3

.= (((1. L) - (q |^ (len f))) + (((q |^ (len f)) * (1. L)) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by VECTSP_1:def 2

.= (((1. L) - (q |^ (len f))) + ((q |^ (len f)) + ((q |^ (len f)) * (- q)))) / ((1. L) - q)

.= ((1. L) + ((- (q |^ (len f))) + ((q |^ (len f)) + ((q |^ (len f)) * (- q))))) / ((1. L) - q) by RLVECT_1:def 3

.= ((1. L) + (((- (q |^ (len f))) + (q |^ (len f))) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by RLVECT_1:def 3

.= ((1. L) + ((0. L) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by RLVECT_1:5

.= ((1. L) + ((q |^ (len f)) * (- q))) / ((1. L) - q) by ALGSTR_1:def 2

.= ((1. L) + (- ((q |^ (len f)) * q))) / ((1. L) - q) by VECTSP_1:8

.= ((1. L) - (q |^ (len s))) / ((1. L) - q) by A13, GROUP_1:def 7 ;

:: thesis: verum

now :: thesis: for s being FinSequence of L st len s = 0 holds

for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s

then A23:
Sfor q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s

let s be FinSequence of L; :: thesis: ( len s = 0 implies for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s )

assume len s = 0 ; :: thesis: for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s

then A22: s = <*> the carrier of L ;

let q be Element of L; :: thesis: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) implies ((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s )

assume that

q <> 1. L and

for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ; :: thesis: ((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s

thus ((1. L) - (q |^ 0)) / ((1. L) - q) = ((1. L) - (1_ L)) / ((1. L) - q) by BINOM:8

.= (0. L) / ((1. L) - q) by RLVECT_1:15

.= 0. L

.= Sum s by A22, RLVECT_1:43 ; :: thesis: verum

end;s . i = q |^ (i -' 1) ) holds

((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s )

assume len s = 0 ; :: thesis: for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) holds

((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s

then A22: s = <*> the carrier of L ;

let q be Element of L; :: thesis: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ) implies ((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s )

assume that

q <> 1. L and

for i being Nat st 1 <= i & i <= len s holds

s . i = q |^ (i -' 1) ; :: thesis: ((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s

thus ((1. L) - (q |^ 0)) / ((1. L) - q) = ((1. L) - (1_ L)) / ((1. L) - q) by BINOM:8

.= (0. L) / ((1. L) - q) by RLVECT_1:15

.= 0. L

.= Sum s by A22, RLVECT_1:43 ; :: thesis: verum

for k being Nat holds S

hence Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) by A1; :: thesis: verum