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

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

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

A15:
k <= k + 1
by NAT_1:11;
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;

end;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))end;

hence
x in (L~ (f | k)) \/ (LSeg (f,k))
; :: thesis: verumper cases
( n + 1 = len f or n + 1 <> len f )
;

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;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

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~ fend;

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

end;

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;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