let F, G, H be FinSequence of REAL ; :: thesis: ( len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ) implies Sum H = (Sum F) + (Sum G) )
assume that
A1: len F = len G and
A2: len F = len H and
A3: for k being Element of NAT st k in dom F holds
H . k = (F /. k) + (G /. k) ; :: thesis: Sum H = (Sum F) + (Sum G)
A4: F is Element of (len F) -tuples_on REAL by FINSEQ_2:92;
A5: G is Element of (len F) -tuples_on REAL by A1, FINSEQ_2:92;
then F + G is Element of (len F) -tuples_on REAL by A4, FINSEQ_2:120;
then A6: len H = len (F + G) by A2, CARD_1:def 7;
then A7: dom H = Seg (len (F + G)) by FINSEQ_1:def 3;
A8: for k being Element of NAT st k in dom F holds
H . k = (F . k) + (G . k)
proof
let k be Element of NAT ; :: thesis: ( k in dom F implies H . k = (F . k) + (G . k) )
assume A9: k in dom F ; :: thesis: H . k = (F . k) + (G . k)
then k in Seg (len G) by A1, FINSEQ_1:def 3;
then k in dom G by FINSEQ_1:def 3;
then A10: G /. k = G . k by PARTFUN1:def 6;
F /. k = F . k by A9, PARTFUN1:def 6;
hence H . k = (F . k) + (G . k) by A3, A9, A10; :: thesis: verum
end;
for k being Nat st k in dom H holds
H . k = (F + G) . k
proof
let k be Nat; :: thesis: ( k in dom H implies H . k = (F + G) . k )
assume A11: k in dom H ; :: thesis: H . k = (F + G) . k
then k in dom F by A2, A6, A7, FINSEQ_1:def 3;
then A12: H . k = (F . k) + (G . k) by A8;
k in dom (F + G) by A7, A11, FINSEQ_1:def 3;
hence H . k = (F + G) . k by A12, VALUED_1:def 1; :: thesis: verum
end;
then Sum H = Sum (F + G) by A6, FINSEQ_2:9
.= (Sum F) + (Sum G) by A4, A5, RVSUM_1:89 ;
hence Sum H = (Sum F) + (Sum G) ; :: thesis: verum