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₁[ Element of 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 Element of NAT st S₁[l] holds
S₁[l + 1]

proof

let l be Element of 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: len g = l by A5, FINSEQ_1:def 3;
A8: 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 A9: ( 1 <= k & k <= l ) ; :: thesis: g /. k = 1. L
then A10: k in dom g by A5, FINSEQ_1:1;
k in Seg l by A9, FINSEQ_1:1;
then 1. L = g . k by A6
.= g /. k by A10, PARTFUN1:def 6 ;
hence g /. k = 1. L ; :: thesis: verum

end;

then A11: 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 A12: 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
A13: len s = l + 1 and
A14: for k being Element of NAT st 1 <= k & k <= l + 1 holds
s /. k = 1. L ; :: thesis: Sum s = (l + 1) * (1. L)
A15: dom s = Seg (l + 1) by A13, FINSEQ_1:def 3;
A16: for k being Nat st k in dom s holds
s . k = (g ^ <*(1. L)*>) . k

proof

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

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

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

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

end;

suppose A23: ( 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 A23, NAT_1:13;
then ( dom <*(1. L)*> = Seg 1 & ii = (k - k) + 1 ) by A23, FINSEQ_1:def 8, XXREAL_0:1;
then A24: ii in dom <*(1. L)*> ;
l + 0 < k + l by A23, XREAL_1:8;
then l + 1 <= k + l by NAT_1:13;
then A25: (l + 1) - l <= (k + l) - l by XREAL_1:9;
l + 1 <= k by A23, NAT_1:13;
then A26: ii = (k - k) + 1 by A23, XXREAL_0:1;
then (g ^ <*(1. L)*>) . k = (g ^ <*(1. L)*>) . ((len g) + ii) by A5, FINSEQ_1:def 3
.= <*(1. L)*> . 1 by A24, A26, FINSEQ_1:def 7
.= 1. L by FINSEQ_1:def 8
.= s /. k by A14, A18, A23, A25
.= s . k by A19, 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, A12, A15, FINSEQ_1:def 3 ;
then s = g ^ <*(1. L)*> by A16, FINSEQ_1:13;
then Sum s = (Sum g) + (1. L) by FVSUM_1:71
.= (l * (1. L)) + (1. L) by A3, A7, A11
.= (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
A27: 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)
A28: <*> the carrier of L is Element of 0 -tuples_on the carrier of L by FINSEQ_2:131;
s = {} by A27;
then Sum s = Sum (<*> the carrier of L)
.= 0. L by A28, FVSUM_1:74
.= 0 * (1. L) by BINOM:12 ;
hence Sum s = 0 * (1. L) ; :: thesis: verum

end;

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