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 b1 being FinSequence of D st
for i being Nat st len f = i + 1 holds
b1 = f | (Seg i) ) & ( not len f > 0 implies ex b1 being FinSequence of D st b1 = {} ) ) by A1; :: thesis: verum