let f be FinSequence of (); :: 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 ;
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 ;
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 ; :: thesis: verum
end;
suppose A10: n + 1 <> len f ; :: thesis: x in (L~ (f | k)) \/ (LSeg (f,k))
A11: 1 <= n + 1 by ;
n <= k by ;
then A12: n in dom (f | k) by ;
A13: n + 1 < len f by ;
then n + 1 <= k by ;
then n + 1 in dom (f | k) by ;
then A14: X = LSeg ((f | k),n) by ;
n + 1 <= k by ;
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 ;
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 ;
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 ;
then A22: n in dom (f | k) by ;
1 <= n + 1 by NAT_1:11;
then n + 1 in dom (f | k) by ;
then A23: X = LSeg (f,n) by ;
n + 1 <= len f by ;
then X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by ;
hence x in L~ f by ; :: 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 ; :: thesis: verum
end;
end;
end;
hence x in L~ f ; :: thesis: verum