let L be non empty right_complementable add-associative right_zeroed left_zeroed doubleLoopStr ; :: thesis: for m being Element of NAT
for s being FinSequence of L st len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L ) holds
Sum s = m * (1. L)
let m be Element of NAT ; :: thesis: for s being FinSequence of L st len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L ) holds
Sum s = m * (1. L)
let s be FinSequence of L; :: thesis: ( len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L ) implies Sum s = m * (1. L) )
assume A1: ( len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L ) ) ; :: thesis: Sum s = m * (1. L)
defpred S₁[ Nat] means for s being FinSequence of L st len s = $1 & ( for k being Element of NAT st 1 <= k & k <= $1 holds
s /. k = 1. L ) holds
Sum s = $1 * (1. L);
A2: for l being Nat st S₁[l] holds
S₁[l + 1]

proof

let l be Nat; :: thesis: ( S₁[l] implies S₁[l + 1] )
assume A3: for g being FinSequence of L st len g = l & ( for k being Element of NAT st 1 <= k & k <= l holds
g /. k = 1. L ) holds
Sum g = l * (1. L) ; :: thesis: S₁[l + 1]
for s being FinSequence of L st len s = l + 1 & ( for k being Element of NAT st 1 <= k & k <= l + 1 holds
s /. k = 1. L ) holds
Sum s = (l + 1) * (1. L)

proof

ex G being FinSequence of L st
( dom G = Seg l & ( for k being Nat st k in Seg l holds
G . k = 1. L ) )

proof

defpred S₂[ Nat, set ] means $2 = 1. L;
A4: for n being Nat st n in Seg l holds
ex x being Element of L st S₂[n,x] ;
ex G being FinSequence of L st
( dom G = Seg l & ( for nn being Nat st nn in Seg l holds
S₂[nn,G . nn] ) ) from FINSEQ_1:sch 5(A4);
hence ex G being FinSequence of L st
( dom G = Seg l & ( for k being Nat st k in Seg l holds
G . k = 1. L ) ) ; :: thesis: verum

end;

then consider g being FinSequence of L such that
A5: dom g = Seg l and
A6: for k being Nat st k in Seg l holds
g . k = 1. L ;
A7: l in NAT by ORDINAL1:def 12;
then A8: len g = l by A5, FINSEQ_1:def 3;
A9: for k being Nat st 1 <= k & k <= l holds
g /. k = 1. L

proof

let k be Nat; :: thesis: ( 1 <= k & k <= l implies g /. k = 1. L )
assume A10: ( 1 <= k & k <= l ) ; :: thesis: g /. k = 1. L
then A11: k in dom g by A5;
k in Seg l by A10;
then 1. L = g . k by A6
.= g /. k by A11, PARTFUN1:def 6 ;
hence g /. k = 1. L ; :: thesis: verum

end;

then A12: for k being Element of NAT st 1 <= k & k <= l holds
g /. k = 1. L ;
dom <*(1. L)*> = Seg 1 by FINSEQ_1:def 8;
then A13: len <*(1. L)*> = 1 by FINSEQ_1:def 3;
let s be FinSequence of L; :: thesis: ( len s = l + 1 & ( for k being Element of NAT st 1 <= k & k <= l + 1 holds
s /. k = 1. L ) implies Sum s = (l + 1) * (1. L) )
assume that
A14: len s = l + 1 and
A15: for k being Element of NAT st 1 <= k & k <= l + 1 holds
s /. k = 1. L ; :: thesis: Sum s = (l + 1) * (1. L)
A16: dom s = Seg (l + 1) by A14, FINSEQ_1:def 3;
A17: for k being Nat st k in dom s holds
s . k = (g ^ <*(1. L)*>) . k

proof

A18: dom s = Seg (l + 1) by A14, FINSEQ_1:def 3;
let k be Nat; :: thesis: ( k in dom s implies s . k = (g ^ <*(1. L)*>) . k )
A19: k in NAT by ORDINAL1:def 12;
assume A20: k in dom s ; :: thesis: s . k = (g ^ <*(1. L)*>) . k

per cases ( ( 1 <= k & k <= l ) or ( l < k & k <= l + 1 ) ) by A20, A18, FINSEQ_1:1;

suppose A21: ( 1 <= k & k <= l ) ; :: thesis: s . k = (g ^ <*(1. L)*>) . k

then A22: k <= l + 1 by NAT_1:12;
A23: k in dom g by A5, A21;
then (g ^ <*(1. L)*>) . k = g . k by FINSEQ_1:def 7
.= g /. k by A23, PARTFUN1:def 6
.= 1. L by A9, A21
.= s /. k by A15, A19, A21, A22
.= s . k by A20, PARTFUN1:def 6 ;
hence s . k = (g ^ <*(1. L)*>) . k ; :: thesis: verum

end;

suppose A24: ( l < k & k <= l + 1 ) ; :: thesis: s . k = (g ^ <*(1. L)*>) . k

then k - k <= (l + 1) - k by XREAL_1:9;
then reconsider ii = ((l + 1) - k) + 1 as Element of NAT by INT_1:3;
l + 1 <= k by A24, NAT_1:13;
then ( dom <*(1. L)*> = Seg 1 & ii = (k - k) + 1 ) by A24, FINSEQ_1:def 8, XXREAL_0:1;
then A25: ii in dom <*(1. L)*> ;
l + 0 < k + l by A24, XREAL_1:8;
then l + 1 <= k + l by NAT_1:13;
then A26: (l + 1) - l <= (k + l) - l by XREAL_1:9;
l + 1 <= k by A24, NAT_1:13;
then A27: ii = (k - k) + 1 by A24, XXREAL_0:1;
then (g ^ <*(1. L)*>) . k = (g ^ <*(1. L)*>) . ((len g) + ii) by A5, FINSEQ_1:def 3, A7
.= <*(1. L)*> . 1 by A25, A27, FINSEQ_1:def 7
.= 1. L by FINSEQ_1:def 8
.= s /. k by A15, A19, A24, A26
.= s . k by A20, PARTFUN1:def 6 ;
hence s . k = (g ^ <*(1. L)*>) . k ; :: thesis: verum

end;

end;

end;

dom (g ^ <*(1. L)*>) = Seg ((len g) + (len <*(1. L)*>)) by FINSEQ_1:def 7
.= dom s by A5, A13, A16, FINSEQ_1:def 3, A7 ;
then s = g ^ <*(1. L)*> by A17, FINSEQ_1:13;
then Sum s = (Sum g) + (1. L) by FVSUM_1:71
.= (l * (1. L)) + (1. L) by A3, A8, A12
.= (l * (1. L)) + (1 * (1. L)) by BINOM:13
.= (l + 1) * (1. L) by BINOM:15 ;
hence Sum s = (l + 1) * (1. L) ; :: thesis: verum

end;

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

end;

for s being FinSequence of L st len s = 0 & ( for k being Element of NAT st 1 <= k & k <= 0 holds
s /. k = 1. L ) holds
Sum s = 0 * (1. L)

proof

let s be FinSequence of L; :: thesis: ( len s = 0 & ( for k being Element of NAT st 1 <= k & k <= 0 holds
s /. k = 1. L ) implies Sum s = 0 * (1. L) )
assume that
A28: len s = 0 and
for k being Element of NAT st 1 <= k & k <= 0 holds
s /. k = 1. L ; :: thesis: Sum s = 0 * (1. L)
A29: <*> the carrier of L is Element of 0 -tuples_on the carrier of L by FINSEQ_2:131;
s = {} by A28;
then Sum s = Sum (<*> the carrier of L)
.= 0. L by A29, FVSUM_1:74
.= 0 * (1. L) by BINOM:12 ;
hence Sum s = 0 * (1. L) ; :: thesis: verum

end;

then A30: S₁[ 0 ] ;
for l being Nat holds S₁[l] from NAT_1:sch 2(A30, A2);
hence Sum s = m * (1. L) by A1; :: thesis: verum