let g, h be FinSequence of D; :: thesis: ( ( len f > 0 & ( for i being Nat st len f = i + 1 holds
g = f | (Seg i) ) & ( for i being 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 Nat st len f = i + 1 holds
g = f | (Seg i) ) & ( for i being Nat st len f = i + 1 holds
h = f | (Seg i) ) implies g = h )

proof

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

end;

hence ( ( len f > 0 & ( for i being Nat st len f = i + 1 holds
g = f | (Seg i) ) & ( for i being 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