let W be Function; :: thesis: for G being Graph
for pe, qe being FinSequence of the carrier' of G st W is_weight_of G holds
cost ((pe ^ qe),W) = (cost (pe,W)) + (cost (qe,W))
let G be Graph; :: thesis: for pe, qe being FinSequence of the carrier' of G st W is_weight_of G holds
cost ((pe ^ qe),W) = (cost (pe,W)) + (cost (qe,W))
let pe, qe be FinSequence of the carrier' of G; :: thesis: ( W is_weight_of G implies cost ((pe ^ qe),W) = (cost (pe,W)) + (cost (qe,W)) )
set r = pe ^ qe;
set f = RealSequence ((pe ^ qe),W);
set g = RealSequence (pe,W);
set h = RealSequence (qe,W);
assume A1: W is_weight_of G ; :: thesis: cost ((pe ^ qe),W) = (cost (pe,W)) + (cost (qe,W))
then A2: dom pe = dom (RealSequence (pe,W)) by Def15;
then A3: len pe = len (RealSequence (pe,W)) by FINSEQ_3:29;
A4: dom qe = dom (RealSequence (qe,W)) by A1, Def15;
then A5: len qe = len (RealSequence (qe,W)) by FINSEQ_3:29;
A6: dom (pe ^ qe) = dom (RealSequence ((pe ^ qe),W)) by A1, Def15;
then len (RealSequence ((pe ^ qe),W)) = len (pe ^ qe) by FINSEQ_3:29;
then A7: len (RealSequence ((pe ^ qe),W)) = (len (RealSequence (pe,W))) + (len (RealSequence (qe,W))) by A3, A5, FINSEQ_1:22;

A8: now :: thesis: for i being Nat st i in dom (RealSequence (qe,W)) holds
(RealSequence ((pe ^ qe),W)) . ((len (RealSequence (pe,W))) + i) = (RealSequence (qe,W)) . i

let i be Nat; :: thesis: ( i in dom (RealSequence (qe,W)) implies (RealSequence ((pe ^ qe),W)) . ((len (RealSequence (pe,W))) + i) = (RealSequence (qe,W)) . i )
assume A9: i in dom (RealSequence (qe,W)) ; :: thesis: (RealSequence ((pe ^ qe),W)) . ((len (RealSequence (pe,W))) + i) = (RealSequence (qe,W)) . i
then 1 <= i by FINSEQ_3:25;
then A10: 1 <= (len (RealSequence (pe,W))) + i by NAT_1:12;
i <= len (RealSequence (qe,W)) by A9, FINSEQ_3:25;
then (len (RealSequence (pe,W))) + i <= len (RealSequence ((pe ^ qe),W)) by A7, XREAL_1:7;
then A11: (len (RealSequence (pe,W))) + i in dom (RealSequence ((pe ^ qe),W)) by A10, FINSEQ_3:25;
( (RealSequence (qe,W)) . i = W . (qe . i) & (pe ^ qe) . ((len (RealSequence (pe,W))) + i) = qe . i ) by A1, A4, A3, A9, Def15, FINSEQ_1:def 7;
hence (RealSequence ((pe ^ qe),W)) . ((len (RealSequence (pe,W))) + i) = (RealSequence (qe,W)) . i by A1, A6, A11, Def15; :: thesis: verum

end;

now :: thesis: for i being Nat st i in dom (RealSequence (pe,W)) holds
(RealSequence ((pe ^ qe),W)) . i = (RealSequence (pe,W)) . i

let i be Nat; :: thesis: ( i in dom (RealSequence (pe,W)) implies (RealSequence ((pe ^ qe),W)) . i = (RealSequence (pe,W)) . i )
assume A12: i in dom (RealSequence (pe,W)) ; :: thesis: (RealSequence ((pe ^ qe),W)) . i = (RealSequence (pe,W)) . i
then i <= len (RealSequence (pe,W)) by FINSEQ_3:25;
then A13: i <= len (RealSequence ((pe ^ qe),W)) by A7, NAT_1:12;
1 <= i by A12, FINSEQ_3:25;
then A14: i in dom (RealSequence ((pe ^ qe),W)) by A13, FINSEQ_3:25;
( (RealSequence (pe,W)) . i = W . (pe . i) & (pe ^ qe) . i = pe . i ) by A1, A2, A12, Def15, FINSEQ_1:def 7;
hence (RealSequence ((pe ^ qe),W)) . i = (RealSequence (pe,W)) . i by A1, A6, A14, Def15; :: thesis: verum

end;

then RealSequence ((pe ^ qe),W) = (RealSequence (pe,W)) ^ (RealSequence (qe,W)) by A7, A8, FINSEQ_3:38;
hence cost ((pe ^ qe),W) = (cost (pe,W)) + (cost (qe,W)) by RVSUM_1:75; :: thesis: verum