let W be Function; :: thesis: 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 Element of NAT st i in dom f holds
f . i >= 0
let G be Graph; :: thesis: 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 Element of NAT st i in dom f holds
f . i >= 0
let pe be FinSequence of the carrier' of G; :: thesis: for f being FinSequence of REAL st W is_weight>=0of G & f = RealSequence (pe,W) holds
for i being Element of NAT st i in dom f holds
f . i >= 0
let f be FinSequence of REAL ; :: thesis: ( W is_weight>=0of G & f = RealSequence (pe,W) implies for i being Element of NAT st i in dom f holds
f . i >= 0 )
assume that
A1: W is_weight>=0of G and
A2: f = RealSequence (pe,W) ; :: thesis: for i being Element of NAT st i in dom f holds
f . i >= 0
A3: W is Function of the carrier' of G,Real>=0 by A1, Def13;
let i be Element of NAT ; :: thesis: ( i in dom f implies f . i >= 0 )
assume A4: i in dom f ; :: thesis: f . i >= 0
A5: W is_weight_of G by A1, Th50;
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 ; :: thesis: verum