theorem Th96: :: HILB10_7:96

for n being Nat
for F being finite set
for E being Enumeration of F st len E = n + 1 holds
( E | n is Enumeration of F \ {(E . (len E))} & <*(E . (len E))*> is Enumeration of {(E . (len E))} & F = (F \ {(E . (len E))}) \/ {(E . (len E))} )