let G be _finite _Graph; :: thesis: for S being VNumberingSeq of G
for n being Nat
for x being set holds
( (S . n) . x <= S .Lifespan() & ( x in dom (S . n) implies 1 <= (S . n) . x ) )
let S be VNumberingSeq of G; :: thesis: for n being Nat
for x being set holds
( (S . n) . x <= S .Lifespan() & ( x in dom (S . n) implies 1 <= (S . n) . x ) )
let n be Nat; :: thesis: for x being set holds
( (S . n) . x <= S .Lifespan() & ( x in dom (S . n) implies 1 <= (S . n) . x ) )
let x be set ; :: thesis: ( (S . n) . x <= S .Lifespan() & ( x in dom (S . n) implies 1 <= (S . n) . x ) )
set CSN = S . n;
set VLN = S . n;

A1: now :: thesis: (S . n) . x <= S .Lifespan()

per cases ( not x in dom (S . n) or x in dom (S . n) ) ;

suppose not x in dom (S . n) ; :: thesis: (S . n) . x <= S .Lifespan()

hence (S . n) . x <= S .Lifespan() by FUNCT_1:def 2; :: thesis: verum

end;

suppose x in dom (S . n) ; :: thesis: (S . n) . x <= S .Lifespan()

then (S . n) . x in rng (S . n) by FUNCT_1:def 3;
then (S . n) . x in (Seg (S .Lifespan())) \ (Seg ((S .Lifespan()) -' n)) by Th14;
hence (S . n) . x <= S .Lifespan() by Th3; :: thesis: verum

end;

end;

end;

now :: thesis: ( x in dom (S . n) implies 1 <= (S . n) . x )

assume x in dom (S . n) ; :: thesis: 1 <= (S . n) . x
then (S . n) . x in rng (S . n) by FUNCT_1:def 3;
then (S . n) . x in (Seg (S .Lifespan())) \ (Seg ((S .Lifespan()) -' n)) by Th14;
then (S .Lifespan()) -' n < (S . n) . x by Th3;
then 0 + 1 <= (S . n) . x by NAT_1:13;
hence 1 <= (S . n) . x ; :: thesis: verum

end;

hence ( (S . n) . x <= S .Lifespan() & ( x in dom (S . n) implies 1 <= (S . n) . x ) ) by A1; :: thesis: verum