let m be Nat; for xseq, yseq being FinSequence of REAL m st len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq holds
ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )
let xseq, yseq be FinSequence of REAL m; ( len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq implies ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) )
assume A1:
( len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq )
; ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )
A2:
( len xseq = len (accum xseq) & xseq . 1 = (accum xseq) . 1 & ( for k being Nat st 1 <= k & k < len xseq holds
(accum xseq) . (k + 1) = ((accum xseq) /. k) + (xseq /. (k + 1)) ) )
by EUCLID_7:def 10;
A3:
Sum xseq = (accum xseq) . (len xseq)
by A1, EUCLID_7:def 11;
set g = accum xseq;
set i = len yseq;
per cases
( len yseq = 0 or len yseq <> 0 )
;
suppose A5:
len yseq <> 0
;
ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )A6:
(
len yseq = len (accum yseq) &
yseq . 1
= (accum yseq) . 1 & ( for
k being
Nat st 1
<= k &
k < len yseq holds
(accum yseq) . (k + 1) = ((accum yseq) /. k) + (yseq /. (k + 1)) ) )
by EUCLID_7:def 10;
A7:
Sum yseq = (accum yseq) . (len yseq)
by A5, EUCLID_7:def 11;
set g0 =
accum yseq;
A8:
len yseq <= len (accum xseq)
by A1, A2, NAT_1:11;
then A9:
len ((accum xseq) | (len yseq)) = len yseq
by FINSEQ_1:59;
A10:
for
k being
Nat st 1
<= k &
k <= len ((accum xseq) | (len yseq)) holds
((accum xseq) | (len yseq)) . k = (accum yseq) . k
proof
defpred S1[
Nat]
means ( 1
<= $1 & $1
<= len ((accum xseq) | (len yseq)) implies
((accum xseq) | (len yseq)) . $1
= (accum yseq) . $1 );
A11:
S1[
0 ]
;
A12:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A13:
S1[
k]
;
S1[k + 1]now ( 1 <= k + 1 & k + 1 <= len ((accum xseq) | (len yseq)) implies ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1) )assume A14:
( 1
<= k + 1 &
k + 1
<= len ((accum xseq) | (len yseq)) )
;
((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1)then A15:
k + 1
<= len yseq
by A8, FINSEQ_1:59;
then
k + 1
in Seg (len yseq)
by A14;
then A16:
(
((accum xseq) | (len yseq)) . (k + 1) = (accum xseq) . (k + 1) &
xseq . (k + 1) = (xseq | (Seg (len yseq))) . (k + 1) )
by FUNCT_1:49;
A17:
k < len yseq
by A15, NAT_1:13;
now ( k <> 0 implies ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1) )assume A18:
k <> 0
;
((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1)then A19:
1
<= k
by NAT_1:14;
then A20:
k in Seg (len yseq)
by A17;
len yseq <= len xseq
by A1, NAT_1:12;
then A21:
k < len xseq
by A17, XXREAL_0:2;
then
(accum xseq) /. k = (accum xseq) . k
by A2, A19, FINSEQ_4:15;
then
(accum xseq) /. k = ((accum xseq) | (len yseq)) . k
by A20, FUNCT_1:49;
then A22:
(accum xseq) /. k = (accum yseq) /. k
by A6, A17, A19, A13, A14, FINSEQ_4:15, NAT_1:13;
k + 1
<= len xseq
by A15, A1, NAT_1:12;
then
xseq /. (k + 1) = xseq . (k + 1)
by A14, FINSEQ_4:15;
then
xseq /. (k + 1) = yseq /. (k + 1)
by A1, A14, A9, A16, FINSEQ_4:15;
then
((accum xseq) /. k) + (xseq /. (k + 1)) = (accum yseq) . (k + 1)
by A6, A17, A18, A22, NAT_1:14;
hence
((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1)
by A2, A16, A18, A21, NAT_1:14;
verum end; hence
((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1)
by A1, A6, A16, EUCLID_7:def 10;
verum end; hence
S1[
k + 1]
;
verum end;
thus
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A11, A12); verum
end;
1
<= len yseq
by A5, NAT_1:14;
then
len yseq in Seg (len yseq)
;
then A23:
len yseq in dom ((accum xseq) | (len yseq))
by A9, FINSEQ_1:def 3;
then
len yseq in dom (accum xseq)
by RELAT_1:57;
then
(accum xseq) . (len yseq) = (accum xseq) /. (len yseq)
by PARTFUN1:def 6;
then
((accum xseq) | (len yseq)) . (len yseq) = (accum xseq) /. (len yseq)
by A23, FUNCT_1:47;
then A24:
(accum yseq) . (len yseq) = (accum xseq) /. (len yseq)
by A6, A9, A10, FINSEQ_1:14;
dom xseq = Seg ((len yseq) + 1)
by A1, FINSEQ_1:def 3;
then
xseq . (len xseq) in rng xseq
by A1, FINSEQ_1:4, FUNCT_1:3;
then reconsider v =
xseq . (len xseq) as
Element of
REAL m ;
take
v
;
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )thus
v = xseq . (len xseq)
;
Sum xseq = (Sum yseq) + vA25:
len yseq < len xseq
by A1, NAT_1:13;
1
<= (len yseq) + 1
by NAT_1:11;
then
((accum xseq) /. (len yseq)) + (xseq /. ((len yseq) + 1)) = (Sum yseq) + v
by A7, A24, A1, FINSEQ_4:15;
hence
Sum xseq = (Sum yseq) + v
by A1, A25, A2, A3, A5, NAT_1:14;
verum end; end;