let F be FinSequence-yielding FinSequence; :: thesis: ( not doms F is empty iff F is non-empty )
thus ( not doms F is empty implies F is non-empty ) :: thesis: ( F is non-empty implies not doms F is empty )

proof

assume not doms F is empty ; :: thesis: F is non-empty
then consider x being object such that
A1: x in doms F ;
consider p being FinSequence such that
A2: ( p = x & len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) ) by A1, Def8;
let d be object ; :: according to FUNCT_1:def 9 :: thesis: ( not d in dom F or not F . d is empty )
assume A3: d in dom F ; :: thesis: not F . d is empty
dom p = dom F by A2, FINSEQ_3:29;
then p . d in dom (F . d) by A2, A3;
hence not F . d is empty ; :: thesis: verum

end;

set L = (len F) |-> 1;
assume A4: F is non-empty ; :: thesis: not doms F is empty
A5: len ((len F) |-> 1) = len F ;
then A6: dom ((len F) |-> 1) = dom F by FINSEQ_3:29;
for i being Nat st i in dom ((len F) |-> 1) holds
((len F) |-> 1) . i in dom (F . i)

proof

let i be Nat; :: thesis: ( i in dom ((len F) |-> 1) implies ((len F) |-> 1) . i in dom (F . i) )
assume A7: i in dom ((len F) |-> 1) ; :: thesis: ((len F) |-> 1) . i in dom (F . i)
A8: ((len F) |-> 1) . i = 1 by A7, FINSEQ_2:57;
not F . i is empty by A4, A7, A6;
then len (F . i) >= 1 by NAT_1:14;
hence ((len F) |-> 1) . i in dom (F . i) by A8, FINSEQ_3:25; :: thesis: verum

end;

hence not doms F is empty by Def8, A5; :: thesis: verum