let g, h be FinSequence of D; :: thesis: ( ( len f > 0 & ( for i being Element of NAT st len f = i + 1 holds
g = f | (Seg i) ) & ( for i being Element of NAT st len f = i + 1 holds
h = f | (Seg i) ) implies g = h ) & ( not len f > 0 & g = {} & h = {} implies g = h ) )
( len f > 0 & ( for i being Element of NAT st len f = i + 1 holds
g = f | (Seg i) ) & ( for i being Element of NAT st len f = i + 1 holds
h = f | (Seg i) ) implies g = h )

proof

assume A4: ( len f > 0 & ( for i being Element of NAT st len f = i + 1 holds
g = f | (Seg i) ) & ( for i being Element of NAT st len f = i + 1 holds
h = f | (Seg i) ) ) ; :: thesis: g = h
then consider j being Nat such that
A5: len f = j + 1 by NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
( g = f | (Seg j) & h = f | (Seg j) ) by A4, A5;
hence g = h ; :: thesis: verum

end;

hence ( ( len f > 0 & ( for i being Element of NAT st len f = i + 1 holds
g = f | (Seg i) ) & ( for i being Element of NAT st len f = i + 1 holds
h = f | (Seg i) ) implies g = h ) & ( not len f > 0 & g = {} & h = {} implies g = h ) ) ; :: thesis: verum