let G be finite _Graph; :: thesis: for S being VNumberingSeq of G
for n, m being Nat st (S .Lifespan()) -' n < m & m <= S .Lifespan() holds
ex v being Vertex of G st
( v in dom (S . n) & (S . n) . v = m )
let S be VNumberingSeq of G; :: thesis: for n, m being Nat st (S .Lifespan()) -' n < m & m <= S .Lifespan() holds
ex v being Vertex of G st
( v in dom (S . n) & (S . n) . v = m )
let n, m be Nat; :: thesis: ( (S .Lifespan()) -' n < m & m <= S .Lifespan() implies ex v being Vertex of G st
( v in dom (S . n) & (S . n) . v = m ) )
assume that
A1: (S .Lifespan()) -' n < m and
A2: m <= S .Lifespan() ; :: thesis: ex v being Vertex of G st
( v in dom (S . n) & (S . n) . v = m )
set CSN = S . n;
set VLN = S . n;
m in (Seg (S .Lifespan())) \ (Seg ((S .Lifespan()) -' n)) by A1, A2, Th3;
then m in rng (S . n) by Th14;
then consider v being set such that
A3: v in dom (S . n) and
A4: m = (S . n) . v by FUNCT_1:def 5;
take v ; :: thesis: ( v is Vertex of G & v in dom (S . n) & (S . n) . v = m )
thus v is Vertex of G by A3; :: thesis: ( v in dom (S . n) & (S . n) . v = m )
thus v in dom (S . n) by A3; :: thesis: (S . n) . v = m
thus (S . n) . v = m by A4; :: thesis: verum