let f be FinSequence of (TOP-REAL 2); for k being Nat st k <> 0 & len f = k + 1 holds
L~ f = (L~ (f | k)) \/ (LSeg (f,k))
let k be Nat; ( 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
; 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))
XBOOLE_0:def 10 (L~ (f | k)) \/ (LSeg (f,k)) c= L~ fproof
let x be
object ;
TARSKI:def 3 ( not x in L~ f or x in (L~ (f | k)) \/ (LSeg (f,k)) )
assume
x in L~ f
;
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 x in (L~ (f | k)) \/ (LSeg (f,k))per cases
( n + 1 = len f or n + 1 <> len f )
;
suppose A10:
n + 1
<> len f
;
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;
verum end;
hence
x in (L~ (f | k)) \/ (LSeg (f,k))
;
verum
end;
A15:
k <= k + 1
by NAT_1:11;
let x be object ; TARSKI:def 3 ( not x in (L~ (f | k)) \/ (LSeg (f,k)) or x in L~ f )
assume A16:
x in (L~ (f | k)) \/ (LSeg (f,k))
; x in L~ f
now x in L~ fper cases
( x in L~ (f | k) or x in LSeg (f,k) )
by A16, XBOOLE_0:def 3;
suppose
x in L~ (f | k)
;
x in L~ fthen 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;
verum end;
hence
x in L~ f
; verum