let G be finite _Graph; :: thesis: for S being VertexScheme of G

for n being non zero Nat st n <= len S holds

not S .followSet n is empty

let S be VertexScheme of G; :: thesis: for n being non zero Nat st n <= len S holds

not S .followSet n is empty

let n be non zero Nat; :: thesis: ( n <= len S implies not S .followSet n is empty )

assume A1: n <= len S ; :: thesis: not S .followSet n is empty

0 + 1 <= n by NAT_1:13;

then A2: (len ((n,(len S)) -cut S)) + n = (len S) + 1 by A1, FINSEQ_6:def 4;

((len S) + 1) - n <> 0 by A1, NAT_1:13;

then (n,(len S)) -cut S <> {} by A2;

hence not S .followSet n is empty ; :: thesis: verum

for n being non zero Nat st n <= len S holds

not S .followSet n is empty

let S be VertexScheme of G; :: thesis: for n being non zero Nat st n <= len S holds

not S .followSet n is empty

let n be non zero Nat; :: thesis: ( n <= len S implies not S .followSet n is empty )

assume A1: n <= len S ; :: thesis: not S .followSet n is empty

0 + 1 <= n by NAT_1:13;

then A2: (len ((n,(len S)) -cut S)) + n = (len S) + 1 by A1, FINSEQ_6:def 4;

((len S) + 1) - n <> 0 by A1, NAT_1:13;

then (n,(len S)) -cut S <> {} by A2;

hence not S .followSet n is empty ; :: thesis: verum