let L be non empty right_complementable add-associative right_zeroed addLoopStr ; 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; ( 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
; Sum r = (r /. 1) + (r /. 2)
A3:
2 in dom r
by A1, FINSEQ_3:25;
1 <= len r
by A1, XXREAL_0:2;
then A4:
1 in dom r
by FINSEQ_3:25;
not r is empty
by A1;
then consider a being Element of L, r1 being FinSequence of L such that
A5:
a = r . 1
and
A6:
r = <*a*> ^ r1
by FINSEQ_3:102;
A7:
len <*a*> = 1
by FINSEQ_1:40;
then A8: r . 2 =
r1 . (2 - 1)
by A1, A6, FINSEQ_1:24
.=
r1 . 1
;
len r = 1 + (len r1)
by A6, A7, FINSEQ_1:22;
then
not r1 is empty
by A1;
then consider b being Element of L, r2 being FinSequence of L such that
A9:
b = r1 . 1
and
A10:
r1 = <*b*> ^ r2
by FINSEQ_3:102;
A11:
len <*b*> = 1
by FINSEQ_1:40;
A12:
now for i being Element of NAT st i in dom r2 holds
r2 . i = 0. Llet i be
Element of
NAT ;
( i in dom r2 implies r2 . i = 0. L )assume A13:
i in dom r2
;
r2 . i = 0. LA14:
1
+ i in dom r1
by A10, A11, A13, FINSEQ_1:28;
1
<= i
by A13, FINSEQ_3:25;
then
1
< 1
+ i
by NAT_1:13;
then A15:
1
+ 1
< 1
+ (1 + i)
by XREAL_1:8;
thus r2 . i =
r1 . (1 + i)
by A10, A11, A13, FINSEQ_1:def 7
.=
r . (1 + (1 + i))
by A6, A7, A14, FINSEQ_1:def 7
.=
0. L
by A2, A6, A7, A14, A15, FINSEQ_1:28
;
verum end;
thus Sum r =
a + (Sum r1)
by A6, FVSUM_1:72
.=
a + (b + (Sum r2))
by A10, FVSUM_1:72
.=
a + (b + (0. L))
by A12, POLYNOM3:1
.=
a + b
by RLVECT_1:def 4
.=
(r /. 1) + b
by A5, A4, PARTFUN1:def 6
.=
(r /. 1) + (r /. 2)
by A9, A3, A8, PARTFUN1:def 6
; verum