let i be Nat; :: thesis: for W being Function
for G being Graph
for pe, qe 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 Nat st
( j in dom pe & (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i )
let W be Function; :: thesis: for G being Graph
for pe, qe 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 Nat st
( j in dom pe & (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i )
let G be Graph; :: thesis: for pe, qe 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 Nat st
( j in dom pe & (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i )
let pe, qe 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 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 Nat st
( j in dom pe & (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i )
set g = RealSequence (qe,W);
consider y being object such that
A4: y in dom pe and
A5: qe . i = pe . y by A1, A3, FUNCT_1:114;
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