let n be Nat; :: thesis: 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))} )
let F be finite set ; :: thesis: 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))} )
let E be Enumeration of F; :: thesis: ( len E = n + 1 implies ( 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))} ) )
assume A1: len E = n + 1 ; :: thesis: ( 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))} )
set L = len E;
A2: rng <*(E . (len E))*> = {(E . (len E))} by FINSEQ_1:38;
A3: E = (E | n) ^ <*(E . (len E))*> by A1, FINSEQ_3:55;
then A4: ( E | n is one-to-one & <*(E . (len E))*> is one-to-one ) by FINSEQ_3:91;
A5: ( F = rng E & rng E = (rng (E | n)) \/ (rng <*(E . (len E))*>) & rng (E | n) misses rng <*(E . (len E))*> ) by A3, FINSEQ_1:31, FINSEQ_3:91, RLAFFIN3:def 1;
then rng (E | n) = F \ {(E . (len E))} by A2, XBOOLE_1:88;
hence ( 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))} ) by A5, FINSEQ_1:38, A4, RLAFFIN3:def 1; :: thesis: verum