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)
A3: 2 in dom r by ;
1 <= len r by ;
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
.= r1 . 1 ;
len r = 1 + (len r1) by ;
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 :: thesis: for i being Element of NAT st i in dom r2 holds
r2 . i = 0. L
let i be Element of NAT ; :: thesis: ( i in dom r2 implies r2 . i = 0. L )
assume A13: i in dom r2 ; :: thesis: r2 . i = 0. L
A14: 1 + i in dom r1 by ;
1 <= i by ;
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
.= r . (1 + (1 + i)) by
.= 0. L by ; :: thesis: verum
end;
thus Sum r = a + (Sum r1) by
.= a + (b + (Sum r2)) by
.= a + (b + (0. L)) by
.= a + b by RLVECT_1:def 4
.= (r /. 1) + b by
.= (r /. 1) + (r /. 2) by ; :: thesis: verum