let i be Element of NAT ; :: thesis: for W being Function
for G being Graph
for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe & W is_weight_of G & i in dom qe holds
ex j being Element of NAT st
( j in dom pe & (RealSequence pe,W) . j = (RealSequence qe,W) . i )
let W be Function; :: thesis: for G being Graph
for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe & W is_weight_of G & i in dom qe holds
ex j being Element of NAT st
( j in dom pe & (RealSequence pe,W) . j = (RealSequence qe,W) . i )
let G be Graph; :: thesis: for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe & W is_weight_of G & i in dom qe holds
ex j being Element of NAT st
( j in dom pe & (RealSequence pe,W) . j = (RealSequence qe,W) . i )
let qe, pe be FinSequence of the carrier' of G; :: thesis: ( rng qe c= rng pe & W is_weight_of G & i in dom qe implies ex j being Element of NAT st
( j in dom pe & (RealSequence pe,W) . j = (RealSequence qe,W) . i ) )
assume that
A1: rng qe c= rng pe and
A2: W is_weight_of G and
A3: i in dom qe ; :: thesis: ex j being Element of NAT st
( j in dom pe & (RealSequence pe,W) . j = (RealSequence qe,W) . i )
set f = RealSequence pe,W;
set g = RealSequence qe,W;
consider y being set such that
A4: y in dom pe and
A5: qe . i = pe . y by A1, A3, Th2;
reconsider j = y as Element of NAT by A4;
take j ; :: thesis: ( j in dom pe & (RealSequence pe,W) . j = (RealSequence qe,W) . i )
thus j in dom pe by A4; :: thesis: (RealSequence pe,W) . j = (RealSequence qe,W) . i
(RealSequence qe,W) . i = W . (qe . i) by A2, A3, Def15;
hence (RealSequence pe,W) . j = (RealSequence qe,W) . i by A2, A4, A5, Def15; :: thesis: verum