let f be FinSequence of (TOP-REAL 2); :: thesis: for k being Nat st k <> 0 & len f = k + 1 holds
L~ f = (L~ (f | k)) \/ (LSeg (f,k))
let k be 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 Nat : ( 1 <= i & i + 1 <= len f ) } ;
set l1 = { (LSeg ((f | k),j)) where j is 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:59;
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 object ; :: 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 Nat : ( 1 <= i & i + 1 <= len f ) } by TARSKI:def 4;
consider n being Nat such that
A7: X = LSeg (f,n) and
A8: 1 <= n and
A9: n + 1 <= len f by A6;

now :: thesis: x in (L~ (f | k)) \/ (LSeg (f,k))

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:6;
then A12: n in dom (f | k) by A4, A8, FINSEQ_3:25;
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:25;
then A14: X = LSeg ((f | k),n) by A7, A12, TOPREAL3:17;
n + 1 <= k by A2, A13, NAT_1:13;
then X in { (LSeg ((f | k),j)) where j is Nat : ( 1 <= j & j + 1 <= len (f | k) ) } by A4, A8, A14;
then x in union { (LSeg ((f | k),j)) where j is 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 object ; :: 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 :: thesis: x in L~ f

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 Nat : ( 1 <= j & j + 1 <= len (f | k) ) } by TARSKI:def 4;
consider n being 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:25;
1 <= n + 1 by NAT_1:11;
then n + 1 in dom (f | k) by A21, FINSEQ_3:25;
then A23: X = LSeg (f,n) by A19, A22, TOPREAL3:17;
n + 1 <= len f by A2, A15, A4, A21, XXREAL_0:2;
then X in { (LSeg (f,i)) where i is 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 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