let F be FinSequence-yielding FinSequence; :: thesis: for p being FinSequence holds
( p in doms F iff ( len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) ) )
let p be FinSequence; :: thesis: ( p in doms F iff ( len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) ) )

hereby :: thesis: ( len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) implies p in doms F )

assume p in doms F ; :: thesis: ( len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) )
then ex q being FinSequence st
( q = p & len q = len F & ( for i being Nat st i in dom q holds
q . i in dom (F . i) ) ) by Def8;
hence ( len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) ) ; :: thesis: verum

end;

thus ( len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) implies p in doms F ) by Def8; :: thesis: verum