set A = App F;
A1: dom (App F) = doms F by Def9;
rng (App F) c= D *

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (App F) or y in D * )
assume A2: y in rng (App F) ; :: thesis: y in D *
consider x being object such that
A3: ( x in dom (App F) & (App F) . x = y ) by A2, FUNCT_1:def 3;
A4: x in doms F by A3, Def9;
consider p being FinSequence such that
A5: ( p = x & len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) ) by A4, Def8;
A6: dom p = dom F by A5, FINSEQ_3:29;
rng ((App F) . p) c= D

proof

let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in rng ((App F) . p) or i in D )
assume A7: i in rng ((App F) . p) ; :: thesis: i in D
len ((App F) . p) = len p by A4, A5, Def9;
then A8: dom ((App F) . p) = dom p by FINSEQ_3:29;
consider j being object such that
A9: ( j in dom ((App F) . p) & ((App F) . p) . j = i ) by A7, FUNCT_1:def 3;
A10: ((App F) . p) . j = (F . j) . (p . j) by A8, A9, A4, A5, Def9;
F . j in rng F by A9, A8, A6, FUNCT_1:def 3;
then F . j is FinSequence of D by FINSEQ_1:def 11;
then A11: rng (F . j) c= D by FINSEQ_1:def 4;
p . j in dom (F . j) by A5, A9, A8;
then (F . j) . (p . j) in rng (F . j) by FUNCT_1:def 3;
hence i in D by A11, A10, A9; :: thesis: verum

end;

then (App F) . p is FinSequence of D by FINSEQ_1:def 4;
hence y in D * by A3, A5, FINSEQ_1:def 11; :: thesis: verum

end;

hence App F is Function of (doms F),(D *) by A1, FUNCT_2:2; :: thesis: verum