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