let W be Function; for G being Graph
for pe being FinSequence of the carrier' of G
for f being FinSequence of REAL st W is_weight>=0of G & f = RealSequence (pe,W) holds
for i being Nat st i in dom f holds
f . i >= 0
let G be Graph; for pe being FinSequence of the carrier' of G
for f being FinSequence of REAL st W is_weight>=0of G & f = RealSequence (pe,W) holds
for i being Nat st i in dom f holds
f . i >= 0
let pe be FinSequence of the carrier' of G; for f being FinSequence of REAL st W is_weight>=0of G & f = RealSequence (pe,W) holds
for i being Nat st i in dom f holds
f . i >= 0
let f be FinSequence of REAL ; ( W is_weight>=0of G & f = RealSequence (pe,W) implies for i being Nat st i in dom f holds
f . i >= 0 )
assume that
A1:
W is_weight>=0of G
and
A2:
f = RealSequence (pe,W)
; for i being Nat st i in dom f holds
f . i >= 0
A3:
W is Function of the carrier' of G,Real>=0
by A1;
let i be Nat; ( i in dom f implies f . i >= 0 )
assume A4:
i in dom f
; f . i >= 0
A5:
W is_weight_of G
by A1, Th44;
then A6:
dom pe = dom f
by A2, Def15;
then
f . i = W . (pe . i)
by A2, A5, A4, Def15;
then
f . i in Real>=0
by A6, A3, A4, FINSEQ_2:11, FUNCT_2:5;
then
ex r being Real st
( f . i = r & r >= 0 )
;
hence
f . i >= 0
; verum