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_{1}[ 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_{1}[l] holds

S_{1}[l + 1]

s /. k = 1. L ) holds

Sum s = 0 * (1. L)_{1}[ 0 ]
;

for l being Nat holds S_{1}[l]
from NAT_1:sch 2(A30, A2);

hence Sum s = m * (1. L) by A1; :: thesis: verum

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

s /. k = 1. L ) holds

Sum s = $1 * (1. L);

A2: for l being Nat st S

S

proof

for s being FinSequence of L st len s = 0 & ( for k being Element of NAT st 1 <= k & k <= 0 holds
let l be Nat; :: thesis: ( S_{1}[l] implies S_{1}[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_{1}[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)_{1}[l + 1]
; :: thesis: verum

end;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

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

hence
S
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 ) )

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

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

.= 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;( dom G = Seg l & ( for k being Nat st k in Seg l holds

G . k = 1. L ) )

proof

then consider g being FinSequence of L such that
defpred S_{2}[ 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_{2}[n,x]
;

ex G being FinSequence of L st

( dom G = Seg l & ( for nn being Nat st nn in Seg l holds

S_{2}[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;A4: for n being Nat st n in Seg l holds

ex x being Element of L st S

ex G being FinSequence of L st

( dom G = Seg l & ( for nn being Nat st nn in Seg l holds

S

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

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

then A12:
for k being Element of NAT st 1 <= k & k <= l holds
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;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

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

dom (g ^ <*(1. L)*>) =
Seg ((len g) + (len <*(1. L)*>))
by FINSEQ_1:def 7
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

end;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;

end;

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;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

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;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

.= 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

s /. k = 1. L ) holds

Sum s = 0 * (1. L)

proof

then A30:
S
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;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

for l being Nat holds S

hence Sum s = m * (1. L) by A1; :: thesis: verum