let f be FinSequence of (TOP-REAL 2); :: thesis: for k being Element of NAT st k <> 0 & len f = k + 1 holds
L~ f = (L~ (f | k)) \/ (LSeg f,k)
let k be Element of NAT ; :: thesis: ( k <> 0 & len f = k + 1 implies L~ f = (L~ (f | k)) \/ (LSeg f,k) )
assume that
A1: k <> 0 and
A2: len f = k + 1 ; :: thesis: L~ f = (L~ (f | k)) \/ (LSeg f,k)
A3: 0 + 1 <= k by A1, NAT_1:13;
set f1 = f | k;
set lf = { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
set l1 = { (LSeg (f | k),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | k) ) } ;
k <= len f by A2, NAT_1:13;
then A4: len (f | k) = k by FINSEQ_1:80;
thus L~ f c= (L~ (f | k)) \/ (LSeg f,k) :: according to XBOOLE_0:def 10 :: thesis: (L~ (f | k)) \/ (LSeg f,k) c= L~ f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ f or x in (L~ (f | k)) \/ (LSeg f,k) )
assume x in L~ f ; :: thesis: x in (L~ (f | k)) \/ (LSeg f,k)
then consider X being set such that
A5: x in X and
A6: X in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by TARSKI:def 4;
consider n being Element of NAT such that
A7: X = LSeg f,n and
A8: 1 <= n and
A9: n + 1 <= len f by A6;

now

per cases ( n + 1 = len f or n + 1 <> len f ) ;

suppose n + 1 = len f ; :: thesis: x in (L~ (f | k)) \/ (LSeg f,k)

hence x in (L~ (f | k)) \/ (LSeg f,k) by A2, A5, A7, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A10: n + 1 <> len f ; :: thesis: x in (L~ (f | k)) \/ (LSeg f,k)

A11: 1 <= n + 1 by A8, NAT_1:13;
n <= k by A2, A9, XREAL_1:8;
then A12: n in dom (f | k) by A4, A8, FINSEQ_3:27;
A13: n + 1 < len f by A9, A10, XXREAL_0:1;
then n + 1 <= k by A2, NAT_1:13;
then n + 1 in dom (f | k) by A4, A11, FINSEQ_3:27;
then A14: X = LSeg (f | k),n by A7, A12, TOPREAL3:24;
n + 1 <= k by A2, A13, NAT_1:13;
then X in { (LSeg (f | k),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | k) ) } by A4, A8, A14;
then x in union { (LSeg (f | k),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | k) ) } by A5, TARSKI:def 4;
hence x in (L~ (f | k)) \/ (LSeg f,k) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in (L~ (f | k)) \/ (LSeg f,k) ; :: thesis: verum

end;

A15: k <= k + 1 by NAT_1:11;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ (f | k)) \/ (LSeg f,k) or x in L~ f )
assume A16: x in (L~ (f | k)) \/ (LSeg f,k) ; :: thesis: x in L~ f

now

per cases ( x in L~ (f | k) or x in LSeg f,k ) by A16, XBOOLE_0:def 3;

suppose x in L~ (f | k) ; :: thesis: x in L~ f

then consider X being set such that
A17: x in X and
A18: X in { (LSeg (f | k),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | k) ) } by TARSKI:def 4;
consider n being Element of NAT such that
A19: X = LSeg (f | k),n and
A20: 1 <= n and
A21: n + 1 <= len (f | k) by A18;
n <= n + 1 by NAT_1:11;
then n <= len (f | k) by A21, XXREAL_0:2;
then A22: n in dom (f | k) by A20, FINSEQ_3:27;
1 <= n + 1 by NAT_1:11;
then n + 1 in dom (f | k) by A21, FINSEQ_3:27;
then A23: X = LSeg f,n by A19, A22, TOPREAL3:24;
n + 1 <= len f by A2, A15, A4, A21, XXREAL_0:2;
then X in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A20, A23;
hence x in L~ f by A17, TARSKI:def 4; :: thesis: verum

end;

suppose A24: x in LSeg f,k ; :: thesis: x in L~ f

LSeg f,k in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A2, A3;
hence x in L~ f by A24, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence x in L~ f ; :: thesis: verum