reconsider f = {} as FinSequence-yielding FinSequence ;
for i being Nat st i in dom f holds
f . i in dom (f . i) ;
then ex p being FinSequence st
( p = f & len p = len f & ( for i being Nat st i in dom p holds
p . i in dom (f . i) ) ) ;
then A1: {} in doms f by Def8;
doms f c= {{}}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in doms f or y in {{}} )
assume y in doms f ; :: thesis: y in {{}}
then ex p being FinSequence st
( p = y & len p = len f & ( for i being Nat st i in dom p holds
p . i in dom (f . i) ) ) by Def8;
then y = f ;
hence y in {{}} by TARSKI:def 1; :: thesis: verum

end;

hence doms {} = {{}} by A1, ZFMISC_1:33; :: thesis: verum