let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; for p being FinSequence of K
for i, j being Nat st i in dom p & j in dom p & i <> j & ( for k being Nat st k in dom p & k <> i & k <> j holds
p . k = 0. K ) holds
Sum p = (p /. i) + (p /. j)
let p be FinSequence of K; for i, j being Nat st i in dom p & j in dom p & i <> j & ( for k being Nat st k in dom p & k <> i & k <> j holds
p . k = 0. K ) holds
Sum p = (p /. i) + (p /. j)
A1:
now for i, j being Nat st i in dom p & j in dom p & i < j & ( for k being Nat st k in dom p & k <> i & k <> j holds
p . k = 0. K ) holds
Sum p = (p /. i) + (p /. j)let i,
j be
Nat;
( i in dom p & j in dom p & i < j & ( for k being Nat st k in dom p & k <> i & k <> j holds
p . k = 0. K ) implies Sum p = (p /. i) + (p /. j) )assume that A2:
i in dom p
and A3:
j in dom p
and A4:
i < j
and A5:
for
k being
Nat st
k in dom p &
k <> i &
k <> j holds
p . k = 0. K
;
Sum p = (p /. i) + (p /. j)A6:
dom p = Seg (len p)
by FINSEQ_1:def 3;
then
(
i in NAT & 1
<= i )
by A2, FINSEQ_1:1;
then A7:
i in Seg i
;
set pI =
p | i;
consider q being
FinSequence such that A8:
p = (p | i) ^ q
by FINSEQ_1:80;
reconsider q =
q as
FinSequence of
K by A8, FINSEQ_1:36;
A9:
i <= len p
by A2, A6, FINSEQ_1:1;
then A10:
len (p | i) = i
by FINSEQ_1:17;
A11:
dom (p | i) = Seg i
by A9, FINSEQ_1:17;
then
not
j in dom (p | i)
by A4, FINSEQ_1:1;
then consider ji being
Nat such that A12:
ji in dom q
and A13:
j = i + ji
by A3, A8, A10, FINSEQ_1:25;
now for k being Nat st k in dom q & k <> ji holds
q . k = 0. Klet k be
Nat;
( k in dom q & k <> ji implies q . k = 0. K )assume that A14:
k in dom q
and A15:
k <> ji
;
q . k = 0. Kreconsider kk =
k as
Element of
NAT by ORDINAL1:def 12;
A16:
i + kk <> i + ji
by A15;
dom q = Seg (len q)
by FINSEQ_1:def 3;
then
k >= 1
by A14, FINSEQ_1:1;
then
k + i >= i + 1
by XREAL_1:7;
then A17:
i + kk <> i
by NAT_1:13;
thus q . k =
p . (i + kk)
by A8, A10, A14, FINSEQ_1:def 7
.=
0. K
by A5, A8, A10, A13, A14, A17, A16, FINSEQ_1:28
;
verum end; then A18:
Sum q =
q . ji
by A12, MATRIX_3:12
.=
p . j
by A8, A10, A12, A13, FINSEQ_1:def 7
.=
p /. j
by A3, PARTFUN1:def 6
;
A19:
Seg i c= Seg (len p)
by A9, FINSEQ_1:5;
now for k being Nat st k in dom (p | i) & k <> i holds
(p | i) . k = 0. Klet k be
Nat;
( k in dom (p | i) & k <> i implies (p | i) . k = 0. K )assume that A20:
k in dom (p | i)
and A21:
k <> i
;
(p | i) . k = 0. Kreconsider kk =
k as
Element of
NAT by ORDINAL1:def 12;
A22:
k <> j
by A4, A11, A20, FINSEQ_1:1;
thus (p | i) . k =
p . kk
by A8, A20, FINSEQ_1:def 7
.=
0. K
by A5, A6, A11, A19, A20, A21, A22
;
verum end; then Sum (p | i) =
(p | i) . i
by A7, A11, MATRIX_3:12
.=
p . i
by A8, A7, A11, FINSEQ_1:def 7
.=
p /. i
by A6, A7, A19, PARTFUN1:def 6
;
hence
Sum p = (p /. i) + (p /. j)
by A8, A18, RLVECT_1:41;
verum end;
let i, j be Nat; ( i in dom p & j in dom p & i <> j & ( for k being Nat st k in dom p & k <> i & k <> j holds
p . k = 0. K ) implies Sum p = (p /. i) + (p /. j) )
assume that
A23:
( i in dom p & j in dom p )
and
A24:
i <> j
and
A25:
for k being Nat st k in dom p & k <> i & k <> j holds
p . k = 0. K
; Sum p = (p /. i) + (p /. j)
A26:
( i < j or j < i )
by A24, XXREAL_0:1;
for k being Nat st k in dom p & k <> j & k <> i holds
p . k = 0. K
by A25;
hence
Sum p = (p /. i) + (p /. j)
by A1, A23, A25, A26; verum