let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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);

now

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 A2: 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
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 ( q <> 1. L & ( 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
A3: s = <*> the carrier of L by A2;
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:28
.= 0. L by VECTSP_1:36
.= Sum s by A3, RLVECT_1:60 ; :: thesis: verum

end;

then A4: S₁[ 0 ] ;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

now

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) )
assume A7: 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)
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 A8: ( 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)
set f = s | (Seg k);
reconsider f = s | (Seg k) as FinSequence by FINSEQ_1:19;
A9: k <= len s by A7, NAT_1:13;
then A10: len f = k by FINSEQ_1:21;

now

let u be set ; :: 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 set such that
A11: ( x in dom f & f . x = u ) by FUNCT_1:def 5;
reconsider x' = x as Element of NAT by A11;
A12: ( 1 <= x' & x' <= len f ) by A11, FINSEQ_3:27;
then x' <= len s by A7, A10, NAT_1:12;
then A13: x in dom s by A12, FINSEQ_3:27;
f . x = s . x by A11, FUNCT_1:70
.= s /. x by A13, PARTFUN1:def 8 ;
hence u in the carrier of L by A11; :: 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;

A14: now

let i be Nat; :: thesis: ( 1 <= i & i <= len f implies f . i = q |^ (i -' 1) )
assume A15: ( 1 <= i & i <= len f ) ; :: thesis: f . i = q |^ (i -' 1)
then A16: i <= len s by A7, A10, NAT_1:13;
i in dom f by A15, FINSEQ_3:27;
hence f . i = s . i by FUNCT_1:70
.= q |^ (i -' 1) by A8, A15, A16 ;
:: thesis: verum

end;

A17: len s = (len f) + 1 by A7, A9, FINSEQ_1:21;
A18: f = s | (dom f) by A9, FINSEQ_1:21;
A19: 1 <= len s by A7, NAT_1:12;
then (len s) - 1 >= 1 - 1 by XREAL_1:11;
then A20: (len s) -' 1 = (len s) - 1 by XREAL_0:def 2
.= ((len f) + 1) - 1 by A7, A9, FINSEQ_1:21 ;

A21: now

assume (1. L) - q = 0. L ; :: thesis: contradiction
then ((1. L) - q) + q = q by ALGSTR_1:def 5;
then (1. L) + ((- q) + q) = q by RLVECT_1:def 6;
then (1. L) + (0. L) = q by RLVECT_1:16;
hence contradiction by A8, RLVECT_1:def 7; :: thesis: verum

end;

len s in dom s by A19, FINSEQ_3:27;
then A22: s /. (len s) = s . (len s) by PARTFUN1:def 8;
hence Sum s = (Sum f) + (s /. (len s)) by A17, A18, RLVECT_1:55
.= (((1. L) - (q |^ (len f))) / ((1. L) - q)) + (s /. (len s)) by A6, A8, A10, A14
.= (((1. L) - (q |^ (len f))) / ((1. L) - q)) + (q |^ (len f)) by A8, A19, A20, A22
.= (((1. L) - (q |^ (len f))) / ((1. L) - q)) + (((q |^ (len f)) * ((1. L) - q)) / ((1. L) - q)) by A21, Th3
.= (((1. L) - (q |^ (len f))) + ((q |^ (len f)) * ((1. L) - q))) / ((1. L) - q) by VECTSP_1:def 12
.= (((1. L) - (q |^ (len f))) + (((q |^ (len f)) * (1. L)) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by VECTSP_1:def 11
.= (((1. L) - (q |^ (len f))) + ((q |^ (len f)) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by VECTSP_1:def 13
.= ((1. L) + ((- (q |^ (len f))) + ((q |^ (len f)) + ((q |^ (len f)) * (- q))))) / ((1. L) - q) by RLVECT_1:def 6
.= ((1. L) + (((- (q |^ (len f))) + (q |^ (len f))) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by RLVECT_1:def 6
.= ((1. L) + ((0. L) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by RLVECT_1:16
.= ((1. L) + ((q |^ (len f)) * (- q))) / ((1. L) - q) by ALGSTR_1:def 5
.= ((1. L) + (- ((q |^ (len f)) * q))) / ((1. L) - q) by VECTSP_1:40
.= ((1. L) - (q |^ (len s))) / ((1. L) - q) by A17, GROUP_1:def 8 ;
:: thesis: verum

end;

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

end;

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