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) )
assume A1: W is_weight_of G ; :: thesis: 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;
A2: ( dom (pe ^ qe) = dom (RealSequence (pe ^ qe),W) & ( for i being Element of NAT st i in dom (pe ^ qe) holds
(RealSequence (pe ^ qe),W) . i = W . ((pe ^ qe) . i) ) ) by A1, Def15;
A3: ( dom pe = dom (RealSequence pe,W) & ( for i being Element of NAT st i in dom pe holds
(RealSequence pe,W) . i = W . (pe . i) ) ) by A1, Def15;
A4: ( dom qe = dom (RealSequence qe,W) & ( for i being Element of NAT st i in dom qe holds
(RealSequence qe,W) . i = W . (qe . i) ) ) by A1, Def15;
then A5: ( len (RealSequence (pe ^ qe),W) = len (pe ^ qe) & len pe = len (RealSequence pe,W) & len qe = len (RealSequence qe,W) ) by A2, A3, FINSEQ_3:31;
then A6: len (RealSequence (pe ^ qe),W) = (len (RealSequence pe,W)) + (len (RealSequence qe,W)) by FINSEQ_1:35;

A7: now

let i be Element of NAT ; :: thesis: ( i in dom (RealSequence pe,W) implies (RealSequence (pe ^ qe),W) . i = (RealSequence pe,W) . i )
assume A8: i in dom (RealSequence pe,W) ; :: thesis: (RealSequence (pe ^ qe),W) . i = (RealSequence pe,W) . i
then A9: ( 1 <= i & i <= len (RealSequence pe,W) ) by FINSEQ_3:27;
A10: (RealSequence pe,W) . i = W . (pe . i) by A3, A8;
A11: (pe ^ qe) . i = pe . i by A3, A8, FINSEQ_1:def 7;
i <= len (RealSequence (pe ^ qe),W) by A6, A9, NAT_1:12;
then i in dom (RealSequence (pe ^ qe),W) by A9, FINSEQ_3:27;
hence (RealSequence (pe ^ qe),W) . i = (RealSequence pe,W) . i by A2, A10, A11; :: thesis: verum

end;

now

let i be Element of NAT ; :: thesis: ( i in dom (RealSequence qe,W) implies (RealSequence (pe ^ qe),W) . ((len (RealSequence pe,W)) + i) = (RealSequence qe,W) . i )
assume A12: i in dom (RealSequence qe,W) ; :: thesis: (RealSequence (pe ^ qe),W) . ((len (RealSequence pe,W)) + i) = (RealSequence qe,W) . i
then A13: ( 1 <= i & i <= len (RealSequence qe,W) ) by FINSEQ_3:27;
A14: (RealSequence qe,W) . i = W . (qe . i) by A4, A12;
A15: (pe ^ qe) . ((len (RealSequence pe,W)) + i) = qe . i by A4, A5, A12, FINSEQ_1:def 7;
A16: 1 <= (len (RealSequence pe,W)) + i by A13, NAT_1:12;
(len (RealSequence pe,W)) + i <= len (RealSequence (pe ^ qe),W) by A6, A13, XREAL_1:9;
then (len (RealSequence pe,W)) + i in dom (RealSequence (pe ^ qe),W) by A16, FINSEQ_3:27;
hence (RealSequence (pe ^ qe),W) . ((len (RealSequence pe,W)) + i) = (RealSequence qe,W) . i by A2, A14, A15; :: thesis: verum

end;

then RealSequence (pe ^ qe),W = (RealSequence pe,W) ^ (RealSequence qe,W) by A6, A7, FINSEQ_3:43;
hence cost (pe ^ qe),W = (cost pe,W) + (cost qe,W) by RVSUM_1:105; :: thesis: verum