consider k being Nat such that
A1: k + 1 = n by NAT_1:6;
consider Q being FinSequence-membered set such that
Q = E ^^ k and
A2: E ^^ n = Q ^ E by Def3, A1;
thus E ^^ n is empty by A2; :: thesis: verum