let m be Element of NAT ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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;
B2: 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 A3: len yseq = 0 ; :: thesis: ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )

then reconsider v = xseq . (len xseq) as Element of REAL m by A1, B2, EUCLID_7:def 10;
take v ; :: thesis: ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )
Sum yseq = 0* m by A3, EUCLID_7:def 11;
hence ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) by A1, A2, B2, A3, RVSUM_1:33; :: thesis: verum

end;

suppose A4: len yseq <> 0 ; :: thesis: ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )

B5: ( 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;
A5: Sum yseq = (accum yseq) . (len yseq) by A4, EUCLID_7:def 11;
set g0 = accum yseq;
A6: len yseq <= len (accum xseq) by A1, A2, NAT_1:11;
then A7: len ((accum xseq) | (len yseq)) = len yseq by FINSEQ_1:80;
A8: for k being Nat st 1 <= k & k <= len ((accum xseq) | (len yseq)) holds
((accum xseq) | (len yseq)) . k = (accum yseq) . k

proof

defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len ((accum xseq) | (len yseq)) implies ((accum xseq) | (len yseq)) . $1 = (accum yseq) . $1 );
A9: S₁[ 0 ] ;

A10: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A11: S₁[k] ; :: thesis: S₁[k + 1]

now

assume A12: ( 1 <= k + 1 & k + 1 <= len ((accum xseq) | (len yseq)) ) ; :: thesis: ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1)
then A13: k + 1 <= len yseq by A6, FINSEQ_1:80;
then k + 1 in Seg (len yseq) by A12;
then A15: ( ((accum xseq) | (len yseq)) . (k + 1) = (accum xseq) . (k + 1) & xseq . (k + 1) = (xseq | (Seg (len yseq))) . (k + 1) ) by FUNCT_1:72;
A16: k < len yseq by A13, NAT_1:13;

now

assume A17: k <> 0 ; :: thesis: ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1)
then A20: 1 <= k by NAT_1:14;
then A18: k in Seg (len yseq) by A16, FINSEQ_1:3;
len yseq <= len xseq by A1, NAT_1:12;
then A19: k < len xseq by A16, XXREAL_0:2;
then (accum xseq) /. k = (accum xseq) . k by A2, A20, FINSEQ_4:24;
then (accum xseq) /. k = ((accum xseq) | (len yseq)) . k by A18, FUNCT_1:72;
then A21: (accum xseq) /. k = (accum yseq) /. k by B5, A16, A20, A11, A12, FINSEQ_4:24, NAT_1:13;
k + 1 <= len xseq by A13, A1, NAT_1:12;
then xseq /. (k + 1) = xseq . (k + 1) by A12, FINSEQ_4:24;
then xseq /. (k + 1) = yseq /. (k + 1) by A1, A12, A7, A15, FINSEQ_4:24;
then ((accum xseq) /. k) + (xseq /. (k + 1)) = (accum yseq) . (k + 1) by B5, A16, A17, A21, NAT_1:14;
hence ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1) by A2, A15, A17, A19, NAT_1:14; :: thesis: verum

end;

hence ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1) by A1, B5, A15, EUCLID_7:def 10; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

thus for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A10); :: thesis: verum

end;

1 <= len yseq by A4, NAT_1:14;
then len yseq in Seg (len yseq) ;
then A22: len yseq in dom ((accum xseq) | (len yseq)) by A7, FINSEQ_1:def 3;
then len yseq in dom (accum xseq) by RELAT_1:86;
then (accum xseq) . (len yseq) = (accum xseq) /. (len yseq) by PARTFUN1:def 8;
then ((accum xseq) | (len yseq)) . (len yseq) = (accum xseq) /. (len yseq) by A22, FUNCT_1:70;
then A23: (accum yseq) . (len yseq) = (accum xseq) /. (len yseq) by B5, A7, A8, FINSEQ_1:18;
dom xseq = Seg ((len yseq) + 1) by A1, FINSEQ_1:def 3;
then xseq . (len xseq) in rng xseq by A1, FINSEQ_1:6, FUNCT_1:12;
then reconsider v = xseq . (len xseq) as Element of REAL m ;
take v ; :: thesis: ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )
thus v = xseq . (len xseq) ; :: thesis: Sum xseq = (Sum yseq) + v
A24: 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 A5, A23, A1, FINSEQ_4:24;
hence Sum xseq = (Sum yseq) + v by A1, A24, A2, B2, A4, NAT_1:14; :: thesis: verum

end;

end;