reconsider E = {} as FinSequence ;
E in doms {} by Th46, TARSKI:def 1;
then len ((App {}) . E) = len E by Def9;
hence (App {}) . {} = {} ; :: thesis: verum