let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for r being FinSequence of L st len r >= 2 & ( for k being Element of NAT st 2 < k & k in dom r holds
r . k = 0. L ) holds
Sum r = (r /. 1) + (r /. 2)
let r be FinSequence of L; :: thesis: ( len r >= 2 & ( for k being Element of NAT st 2 < k & k in dom r holds
r . k = 0. L ) implies Sum r = (r /. 1) + (r /. 2) )
assume that
A1:
len r >= 2
and
A2:
for k being Element of NAT st 2 < k & k in dom r holds
r . k = 0. L
; :: thesis: Sum r = (r /. 1) + (r /. 2)
not r is empty
by A1;
then consider a being Element of L, r1 being FinSequence of L such that
A3:
a = r . 1
and
A4:
r = <*a*> ^ r1
by FINSEQ_3:111;
A5:
len <*a*> = 1
by FINSEQ_1:57;
then A6:
len r = 1 + (len r1)
by A4, FINSEQ_1:35;
then consider b being Element of L, r2 being FinSequence of L such that
A7:
b = r1 . 1
and
A8:
r1 = <*b*> ^ r2
by FINSEQ_3:111;
A9:
len <*b*> = 1
by FINSEQ_1:57;
A10:
now let i be
Element of
NAT ;
:: thesis: ( i in dom r2 implies r2 . i = 0. L )assume A11:
i in dom r2
;
:: thesis: r2 . i = 0. LA12:
1
+ i in dom r1
by A8, A9, A11, FINSEQ_1:41;
1
<= i
by A11, FINSEQ_3:27;
then
1
< 1
+ i
by NAT_1:13;
then A13:
1
+ 1
< 1
+ (1 + i)
by XREAL_1:10;
thus r2 . i =
r1 . (1 + i)
by A8, A9, A11, FINSEQ_1:def 7
.=
r . (1 + (1 + i))
by A4, A5, A12, FINSEQ_1:def 7
.=
0. L
by A2, A4, A5, A12, A13, FINSEQ_1:41
;
:: thesis: verum end;
1 <= len r
by A1, XXREAL_0:2;
then A14:
1 in dom r
by FINSEQ_3:27;
A15:
2 in dom r
by A1, FINSEQ_3:27;
A16: r . 2 =
r1 . (2 - 1)
by A1, A4, A5, FINSEQ_1:37
.=
r1 . 1
;
thus Sum r =
a + (Sum r1)
by A4, FVSUM_1:89
.=
a + (b + (Sum r2))
by A8, FVSUM_1:89
.=
a + (b + (0. L))
by A10, POLYNOM3:1
.=
a + b
by RLVECT_1:def 7
.=
(r /. 1) + b
by A3, A14, PARTFUN1:def 8
.=
(r /. 1) + (r /. 2)
by A7, A15, A16, PARTFUN1:def 8
; :: thesis: verum