now :: thesis: not {} in rng (App F)

assume {} in rng (App F) ; :: thesis: contradiction
then consider x being object such that
A1: ( x in dom (App F) & (App F) . x = {} ) by FUNCT_1:def 3;
reconsider x = x as FinSequence by A1;
( len ((App F) . x) = len x & len x = len F ) by A1, Th47, Def9;
hence contradiction by A1; :: thesis: verum

end;

hence App F is non-empty by RELAT_1:def 9; :: thesis: verum