A1: ( len f > 0 implies ex g being FinSequence of D st
for i being Nat st len f = i + 1 holds
g = f | (Seg i) )

proof

assume len f > 0 ; :: thesis: ex g being FinSequence of D st
for i being Nat st len f = i + 1 holds
g = f | (Seg i)
then consider j being Nat such that
A2: len f = j + 1 by NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
take g = f | (Seg j); :: thesis: ( g is FinSequence of D & ( for i being Nat st len f = i + 1 holds
g = f | (Seg i) ) )
reconsider g = g as FinSequence by FINSEQ_1:15;

now :: thesis: for a being object st a in rng g holds
a in D

A3: rng g c= rng f by RELAT_1:70;
let a be object ; :: thesis: ( a in rng g implies a in D )
assume a in rng g ; :: thesis: a in D
then a in rng f by A3;
hence a in D ; :: thesis: verum

end;

then rng g c= D ;
then reconsider g = g as FinSequence of D by FINSEQ_1:def 4;
for i being Nat st len f = i + 1 holds
g = f | (Seg i) by A2;
hence ( g is FinSequence of D & ( for i being Nat st len f = i + 1 holds
g = f | (Seg i) ) ) ; :: thesis: verum

end;

<*> D = {} ;
hence ( ( len f > 0 implies ex b₁ being FinSequence of D st
for i being Nat st len f = i + 1 holds
b₁ = f | (Seg i) ) & ( not len f > 0 implies ex b₁ being FinSequence of D st b₁ = {} ) ) by A1; :: thesis: verum