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 )

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

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

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

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