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;

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() end;

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

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;then (S . n) . x in (Seg (S .Lifespan())) \ (Seg ((S .Lifespan()) -' n)) by Th14;

hence (S . n) . x <= S .Lifespan() by Th3; :: thesis: verum

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

hence
( (S . n) . x <= S .Lifespan() & ( x in dom (S . n) implies 1 <= (S . n) . x ) )
by A1; :: thesis: verumassume
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;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