let p, q be FinSequence of REAL ; :: thesis: ( len p <= len q & ( for i being Nat st i in dom q holds
( ( i <= len p implies q . i = p . i ) & ( len p < i implies q . i = 0 ) ) ) implies Sum q = Sum p )
assume that
A1: len p <= len q and
A2: for i being Nat st i in dom q holds
( ( i <= len p implies q . i = p . i ) & ( len p < i implies q . i = 0 ) ) ; :: thesis: Sum q = Sum p
(len q) - (len p) is Nat by A1, NAT_1:21;
then consider ix being Nat such that
A3: ix = (len q) - (len p) ;
set x = ix |-> 0;
A5: Sum (ix |-> 0) = 0 by RVSUM_1:81;
q = p ^ (ix |-> 0)
proof
A6: len (ix |-> 0) = ix by Th4;
then A7: len q = (len p) + (len (ix |-> 0)) by A3;
A8: dom q = Seg ((len p) + (len (ix |-> 0))) by A3, A6, FINSEQ_1:def 3;
A9: for i being Nat st i in dom p holds
q . i = p . i
proof
let i be Nat; :: thesis: ( i in dom p implies q . i = p . i )
assume i in dom p ; :: thesis: q . i = p . i
then A10: ( 1 <= i & i <= len p ) by FINSEQ_3:25;
then ( 1 <= i & i <= len q ) by A1, XXREAL_0:2;
then i in dom q by FINSEQ_3:25;
hence q . i = p . i by A2, A10; :: thesis: verum
end;
for i being Nat st i in dom (ix |-> 0) holds
q . ((len p) + i) = (ix |-> 0) . i
proof
let i be Nat; :: thesis: ( i in dom (ix |-> 0) implies q . ((len p) + i) = (ix |-> 0) . i )
assume i in dom (ix |-> 0) ; :: thesis: q . ((len p) + i) = (ix |-> 0) . i
then A11: i in Seg ix by FUNCOP_1:13;
then A12: (ix |-> 0) . i = 0 by FINSEQ_2:57;
consider j being Nat such that
A13: j = (len p) + i ;
A14: i >= 1 by A11, FINSEQ_1:1;
then A15: len p < j by A13, NAT_1:19;
A16: 0 + 1 <= j by A13, A14, INT_1:7;
i <= len (ix |-> 0) by A6, A11, FINSEQ_1:1;
then j <= len q by A7, A13, XREAL_1:6;
then j in dom q by A16, FINSEQ_3:25;
hence q . ((len p) + i) = (ix |-> 0) . i by A2, A12, A13, A15; :: thesis: verum
end;
hence q = p ^ (ix |-> 0) by A8, A9, FINSEQ_1:def 7; :: thesis: verum
end;
then Sum q = (Sum p) + (Sum (ix |-> 0)) by RVSUM_1:75
.= Sum p by A5 ;
hence Sum q = Sum p ; :: thesis: verum