A1: ( len f > 0 implies ex g being FinSequence of D st
for i being Element of 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 Element of 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 13;
take g = f | (Seg j); :: thesis: ( g is FinSequence of D & ( for i being Element of NAT st len f = i + 1 holds
g = f | (Seg i) ) )
reconsider g = g as FinSequence by FINSEQ_1:19;

now

A3: rng g c= rng f by RELAT_1:99;
let a be set ; :: 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 by TARSKI:def 3;
then reconsider g = g as FinSequence of D by FINSEQ_1:def 4;
for i being Element of NAT st len f = i + 1 holds
g = f | (Seg i) by A2;
hence ( g is FinSequence of D & ( for i being Element of 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 Element of 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