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:31;
A4: dom qe = dom (RealSequence qe,W) by A1, Def15;
then A5: len qe = len (RealSequence qe,W) by FINSEQ_3:31;
A6: dom (pe ^ qe) = dom (RealSequence (pe ^ qe),W) by A1, Def15;
then len (RealSequence (pe ^ qe),W) = len (pe ^ qe) by FINSEQ_3:31;
then A7: len (RealSequence (pe ^ qe),W) = (len (RealSequence pe,W)) + (len (RealSequence qe,W)) by A3, A5, FINSEQ_1:35;

A8: 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 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:27;
then A10: 1 <= (len (RealSequence pe,W)) + i by NAT_1:12;
i <= len (RealSequence qe,W) by A9, FINSEQ_3:27;
then (len (RealSequence pe,W)) + i <= len (RealSequence (pe ^ qe),W) by A7, XREAL_1:9;
then A11: (len (RealSequence pe,W)) + i in dom (RealSequence (pe ^ qe),W) by A10, FINSEQ_3:27;
( (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

let i be Element of 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:27;
then A13: i <= len (RealSequence (pe ^ qe),W) by A7, NAT_1:12;
1 <= i by A12, FINSEQ_3:27;
then A14: i in dom (RealSequence (pe ^ qe),W) by A13, FINSEQ_3:27;
( (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:43;
hence cost (pe ^ qe),W = (cost pe,W) + (cost qe,W) by RVSUM_1:105; :: thesis: verum