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₁[ 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₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]

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)

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;

now :: thesis: for u being object st u in rng f holds
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;

then rng f c= the carrier of L by TARSKI:def 3;
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

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;

(len s) - 1 >= 1 - 1 by A5, XREAL_1:9;
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)

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;

f = s | (dom f) by 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;

hence S₁[k + 1] ; :: thesis: verum

end;

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

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;

then A23: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A23, A2);
hence Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) by A1; :: thesis: verum