let m be 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;
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 A4: 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, A3, EUCLID_7:def 10;
take v ; :: thesis: ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )
Sum yseq = 0* m by A4, EUCLID_7:def 11;
hence ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v ) by A1, A2, A3, A4, RVSUM_1:16; :: thesis: verum
end;
suppose A5: len yseq <> 0 ; :: thesis: 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 :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A13: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( 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)) ) ; :: thesis: ((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 :: thesis: ( k <> 0 implies ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1) )
assume A18: k <> 0 ; :: thesis: ((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; :: thesis: verum
end;
hence ((accum xseq) | (len yseq)) . (k + 1) = (accum yseq) . (k + 1) by A1, A6, A16, EUCLID_7:def 10; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A11, A12); :: thesis: 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 ; :: thesis: ( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )
thus v = xseq . (len xseq) ; :: thesis: Sum xseq = (Sum yseq) + v
A25: 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; :: thesis: verum
end;
end;