let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; for F, G being FinSequence of V st len F = len G & ( for k being Nat
for v being Element of V st k in dom F & v = G . k holds
F . k = - v ) holds
Sum F = - (Sum G)
let F, G be FinSequence of V; ( len F = len G & ( for k being Nat
for v being Element of V st k in dom F & v = G . k holds
F . k = - v ) implies Sum F = - (Sum G) )
defpred S1[ set ] means for H, I being FinSequence of V st len H = len I & len H = $1 & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I);
A1:
dom F = Seg (len F)
by FINSEQ_1:def 3;
now for n being Nat st ( for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I) ) holds
for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I)let n be
Nat;
( ( for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I) ) implies for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I) )assume A2:
for
H,
I being
FinSequence of
V st
len H = len I &
len H = n & ( for
k being
Nat for
v being
Element of
V st
k in Seg (len H) &
v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I)
;
for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I)let H,
I be
FinSequence of
V;
( len H = len I & len H = n + 1 & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) implies Sum H = - (Sum I) )assume that A3:
len H = len I
and A4:
len H = n + 1
and A5:
for
k being
Nat for
v being
Element of
V st
k in Seg (len H) &
v = I . k holds
H . k = - v
;
Sum H = - (Sum I)reconsider p =
H | (Seg n),
q =
I | (Seg n) as
FinSequence of the
carrier of
V by FINSEQ_1:18;
A6:
n <= n + 1
by NAT_1:12;
then A7:
len q = n
by A3, A4, FINSEQ_1:17;
A8:
len p = n
by A4, A6, FINSEQ_1:17;
A9:
now for k being Nat
for v being Element of V st k in Seg (len p) & v = q . k holds
p . k = - v
len p <= len H
by A4, A6, FINSEQ_1:17;
then A10:
Seg (len p) c= Seg (len H)
by FINSEQ_1:5;
A11:
dom p = Seg n
by A4, A6, FINSEQ_1:17;
let k be
Nat;
for v being Element of V st k in Seg (len p) & v = q . k holds
p . k = - vlet v be
Element of
V;
( k in Seg (len p) & v = q . k implies p . k = - v )assume that A12:
k in Seg (len p)
and A13:
v = q . k
;
p . k = - v
dom q = Seg n
by A3, A4, A6, FINSEQ_1:17;
then
I . k = q . k
by A8, A12, FUNCT_1:47;
then
H . k = - v
by A5, A12, A13, A10;
hence
p . k = - v
by A8, A12, A11, FUNCT_1:47;
verum end;
1
<= n + 1
by NAT_1:11;
then
(
n + 1
in dom H &
n + 1
in dom I )
by A3, A4, FINSEQ_3:25;
then reconsider v1 =
H . (n + 1),
v2 =
I . (n + 1) as
Element of
V by FUNCT_1:102;
A14:
v1 = - v2
by A4, A5, FINSEQ_1:4;
A15:
dom q = Seg (len q)
by FINSEQ_1:def 3;
dom p = Seg (len p)
by FINSEQ_1:def 3;
hence Sum H =
(Sum p) + v1
by A4, A8, Th38
.=
(- (Sum q)) + (- v2)
by A2, A8, A7, A9, A14
.=
- ((Sum q) + v2)
by Lm3
.=
- (Sum I)
by A3, A4, A7, A15, Th38
;
verum end;
then A16:
for n being Nat st S1[n] holds
S1[n + 1]
;
then A18:
S1[ 0 ]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A18, A16);
hence
( len F = len G & ( for k being Nat
for v being Element of V st k in dom F & v = G . k holds
F . k = - v ) implies Sum F = - (Sum G) )
by A1; verum