let W be Function; 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; 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; ( 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
; 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 for i being Nat st i in dom (RealSequence (qe,W)) holds
(RealSequence ((pe ^ qe),W)) . ((len (RealSequence (pe,W))) + i) = (RealSequence (qe,W)) . ilet i be
Nat;
( 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))
;
(RealSequence ((pe ^ qe),W)) . ((len (RealSequence (pe,W))) + i) = (RealSequence (qe,W)) . ithen
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;
verum end;
now for i being Nat st i in dom (RealSequence (pe,W)) holds
(RealSequence ((pe ^ qe),W)) . i = (RealSequence (pe,W)) . ilet i be
Nat;
( i in dom (RealSequence (pe,W)) implies (RealSequence ((pe ^ qe),W)) . i = (RealSequence (pe,W)) . i )assume A12:
i in dom (RealSequence (pe,W))
;
(RealSequence ((pe ^ qe),W)) . i = (RealSequence (pe,W)) . ithen
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;
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; verum