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: S₁[ 0 ]

proof

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 A3: ( len s = 0 & ( for k being Element of NAT st 1 <= k & k <= 0 holds
s /. k = 1. L ) ) ; :: thesis: Sum s = 0 * (1. L)
A4: <*> the carrier of L is Element of 0 -tuples_on the carrier of L by FINSEQ_2:114;
s = {} by A3;
then Sum s = Sum (<*> the carrier of L)
.= 0. L by A4, FVSUM_1:93
.= 0 * (1. L) by BINOM:13 ;
hence Sum s = 0 * (1. L) ; :: thesis: verum

end;

hence S₁[ 0 ] ; :: thesis: verum

end;

A5: 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 A6: 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

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 A7: ( len s = l + 1 & ( for k being Element of NAT st 1 <= k & k <= l + 1 holds
s /. k = 1. L ) ) ; :: thesis: Sum s = (l + 1) * (1. L)
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;
A8: 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(A8);
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
A9: ( dom g = Seg l & ( for k being Nat st k in Seg l holds
g . k = 1. L ) ) ;
A10: 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 A11: ( 1 <= k & k <= l ) ; :: thesis: g /. k = 1. L
then A12: k in Seg l by FINSEQ_1:3;
A13: k in dom g by A9, A11, FINSEQ_1:3;
1. L = g . k by A9, A12
.= g /. k by A13, PARTFUN1:def 8 ;
hence g /. k = 1. L ; :: thesis: verum

end;

then A14: ( len g = l & ( for k being Element of NAT st 1 <= k & k <= l holds
g /. k = 1. L ) ) by A9, FINSEQ_1:def 3;
s = g ^ <*(1. L)*>

proof

dom <*(1. L)*> = Seg 1 by FINSEQ_1:def 8;
then A15: len <*(1. L)*> = 1 by FINSEQ_1:def 3;
A16: dom s = Seg (l + 1) by A7, FINSEQ_1:def 3;
A17: dom (g ^ <*(1. L)*>) = Seg ((len g) + (len <*(1. L)*>)) by FINSEQ_1:def 7
.= dom s by A9, A15, A16, FINSEQ_1:def 3 ;
for k being Nat st k in dom s holds
s . k = (g ^ <*(1. L)*>) . k

proof

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

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

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

then A22: k in dom g by A9, A18;
A23: ( 1 <= k & k <= l + 1 ) by A21, NAT_1:12;
(g ^ <*(1. L)*>) . k = g . k by A22, FINSEQ_1:def 7
.= g /. k by A22, PARTFUN1:def 8
.= 1. L by A10, A21
.= s /. k by A7, A18, A23
.= s . k by A19, PARTFUN1:def 8 ;
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:11;
then (l + 1) - k is Element of NAT by INT_1:16;
then reconsider ii = ((l + 1) - k) + 1 as Element of NAT by INT_1:16;
A25: dom <*(1. L)*> = Seg 1 by FINSEQ_1:def 8;
( l + 1 <= k & k <= l + 1 ) by A24, NAT_1:13;
then ii = (k - k) + 1 by XXREAL_0:1;
then A26: ii in dom <*(1. L)*> by A25;
( l + 1 <= k & k <= l + 1 ) by A24, NAT_1:13;
then A27: ii = (k - k) + 1 by XXREAL_0:1;
l + 0 < k + l by A24, XREAL_1:10;
then l + 1 <= k + l by NAT_1:13;
then A28: (l + 1) - l <= (k + l) - l by XREAL_1:11;
(g ^ <*(1. L)*>) . k = (g ^ <*(1. L)*>) . ((len g) + ii) by A9, A27, FINSEQ_1:def 3
.= <*(1. L)*> . 1 by A26, A27, FINSEQ_1:def 7
.= 1. L by FINSEQ_1:def 8
.= s /. k by A7, A18, A24, A28
.= s . k by A19, PARTFUN1:def 8 ;
hence s . k = (g ^ <*(1. L)*>) . k ; :: thesis: verum

end;

end;

end;

hence s = g ^ <*(1. L)*> by A17, FINSEQ_1:17; :: thesis: verum

end;

then Sum s = (Sum g) + (1. L) by FVSUM_1:87
.= (l * (1. L)) + (1. L) by A6, A14
.= (l * (1. L)) + (1 * (1. L)) by BINOM:14
.= (l + 1) * (1. L) by BINOM:16 ;
hence Sum s = (l + 1) * (1. L) ; :: thesis: verum

end;

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

end;

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