let h be FinSequence of (TOP-REAL 2); for i1, i2 being Nat st 1 <= i1 & i1 <= len h & 1 <= i2 & i2 <= len h holds
L~ (mid (h,i1,i2)) c= L~ h
let i1, i2 be Nat; ( 1 <= i1 & i1 <= len h & 1 <= i2 & i2 <= len h implies L~ (mid (h,i1,i2)) c= L~ h )
assume that
A1:
1 <= i1
and
A2:
i1 <= len h
and
A3:
1 <= i2
and
A4:
i2 <= len h
; L~ (mid (h,i1,i2)) c= L~ h
thus
L~ (mid (h,i1,i2)) c= L~ h
verumproof
let x be
object ;
TARSKI:def 3 ( not x in L~ (mid (h,i1,i2)) or x in L~ h )
assume A5:
x in L~ (mid (h,i1,i2))
;
x in L~ h
now ( ( i1 <= i2 & x in L~ h ) or ( i1 > i2 & x in L~ h ) )per cases
( i1 <= i2 or i1 > i2 )
;
case A6:
i1 <= i2
;
x in L~ h
x in union { (LSeg ((mid (h,i1,i2)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (mid (h,i1,i2)) ) }
by A5, TOPREAL1:def 4;
then consider Y being
set such that A7:
(
x in Y &
Y in { (LSeg ((mid (h,i1,i2)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (mid (h,i1,i2)) ) } )
by TARSKI:def 4;
consider i being
Nat such that A8:
Y = LSeg (
(mid (h,i1,i2)),
i)
and A9:
1
<= i
and A10:
i + 1
<= len (mid (h,i1,i2))
by A7;
A11:
LSeg (
(mid (h,i1,i2)),
i)
= LSeg (
((mid (h,i1,i2)) /. i),
((mid (h,i1,i2)) /. (i + 1)))
by A9, A10, TOPREAL1:def 3;
i <= i + 1
by NAT_1:11;
then A12:
i <= len (mid (h,i1,i2))
by A10, XXREAL_0:2;
then A13:
(mid (h,i1,i2)) . i = h . ((i + i1) -' 1)
by A1, A2, A3, A4, A6, A9, FINSEQ_6:118;
A14:
(mid (h,i1,i2)) /. i = (mid (h,i1,i2)) . i
by A9, A12, FINSEQ_4:15;
A15:
(mid (h,i1,i2)) /. (i + 1) = (mid (h,i1,i2)) . (i + 1)
by A10, FINSEQ_4:15, NAT_1:11;
1
+ 1
<= i + i1
by A1, A9, XREAL_1:7;
then A16:
(1 + 1) - 1
<= (i + i1) - 1
by XREAL_1:9;
then A17:
1
<= (i + i1) -' 1
by A1, NAT_D:37;
(i + i1) -' 1
<= ((i + i1) -' 1) + 1
by NAT_1:11;
then
(i + i1) -' 1
<= ((i + i1) - 1) + 1
by A1, NAT_D:37;
then A18:
1
<= i + i1
by A17, XXREAL_0:2;
1
<= i + 1
by NAT_1:11;
then A19:
(mid (h,i1,i2)) . (i + 1) = h . (((i + 1) + i1) -' 1)
by A1, A2, A3, A4, A6, A10, FINSEQ_6:118;
A20:
((i + 1) + i1) -' 1 =
((i + 1) + i1) - 1
by A1, NAT_D:37
.=
i + i1
;
then A21:
((i + 1) + i1) -' 1 =
((i + i1) - 1) + 1
.=
((i + i1) -' 1) + 1
by A1, NAT_D:37
;
len (mid (h,i1,i2)) = (i2 -' i1) + 1
by A1, A2, A3, A4, A6, FINSEQ_6:118;
then
(i + 1) - 1
<= ((i2 -' i1) + 1) - 1
by A10, XREAL_1:9;
then
i <= i2 - i1
by A6, XREAL_1:233;
then A22:
i + i1 <= (i2 - i1) + i1
by XREAL_1:6;
then A23:
i + i1 <= len h
by A4, XXREAL_0:2;
A24:
i + i1 <= len h
by A4, A22, XXREAL_0:2;
then
h /. ((i + i1) -' 1) = h . ((i + i1) -' 1)
by A17, FINSEQ_4:15, NAT_D:44;
then LSeg (
(mid (h,i1,i2)),
i) =
LSeg (
(h /. ((i + i1) -' 1)),
(h /. (((i + 1) + i1) -' 1)))
by A11, A13, A19, A14, A15, A20, A18, A23, FINSEQ_4:15
.=
LSeg (
h,
((i + i1) -' 1))
by A16, A24, A20, A21, TOPREAL1:def 3
;
then
LSeg (
(mid (h,i1,i2)),
i)
in { (LSeg (h,j)) where j is Nat : ( 1 <= j & j + 1 <= len h ) }
by A16, A20, A21, A23;
then
x in union { (LSeg (h,j)) where j is Nat : ( 1 <= j & j + 1 <= len h ) }
by A7, A8, TARSKI:def 4;
hence
x in L~ h
by TOPREAL1:def 4;
verum end; case A25:
i1 > i2
;
x in L~ h
mid (
h,
i1,
i2)
= Rev (mid (h,i2,i1))
by FINSEQ_6:196;
then
x in L~ (mid (h,i2,i1))
by A5, SPPOL_2:22;
then
x in union { (LSeg ((mid (h,i2,i1)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (mid (h,i2,i1)) ) }
by TOPREAL1:def 4;
then consider Y being
set such that A26:
(
x in Y &
Y in { (LSeg ((mid (h,i2,i1)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (mid (h,i2,i1)) ) } )
by TARSKI:def 4;
consider i being
Nat such that A27:
Y = LSeg (
(mid (h,i2,i1)),
i)
and A28:
1
<= i
and A29:
i + 1
<= len (mid (h,i2,i1))
by A26;
A30:
LSeg (
(mid (h,i2,i1)),
i)
= LSeg (
((mid (h,i2,i1)) /. i),
((mid (h,i2,i1)) /. (i + 1)))
by A28, A29, TOPREAL1:def 3;
i <= i + 1
by NAT_1:11;
then A31:
i <= len (mid (h,i2,i1))
by A29, XXREAL_0:2;
then A32:
(mid (h,i2,i1)) . i = h . ((i + i2) -' 1)
by A1, A2, A3, A4, A25, A28, FINSEQ_6:118;
A33:
(mid (h,i2,i1)) /. i = (mid (h,i2,i1)) . i
by A28, A31, FINSEQ_4:15;
A34:
(mid (h,i2,i1)) /. (i + 1) = (mid (h,i2,i1)) . (i + 1)
by A29, FINSEQ_4:15, NAT_1:11;
1
+ 1
<= i + i2
by A3, A28, XREAL_1:7;
then A35:
(1 + 1) - 1
<= (i + i2) - 1
by XREAL_1:9;
then A36:
1
<= (i + i2) -' 1
by A3, NAT_D:37;
(i + i2) -' 1
<= ((i + i2) -' 1) + 1
by NAT_1:11;
then
(i + i2) -' 1
<= ((i + i2) - 1) + 1
by A3, NAT_D:37;
then A37:
1
<= i + i2
by A36, XXREAL_0:2;
1
<= i + 1
by NAT_1:11;
then A38:
(mid (h,i2,i1)) . (i + 1) = h . (((i + 1) + i2) -' 1)
by A1, A2, A3, A4, A25, A29, FINSEQ_6:118;
A39:
((i + 1) + i2) -' 1 =
((i + 1) + i2) - 1
by A3, NAT_D:37
.=
i + i2
;
then A40:
((i + 1) + i2) -' 1 =
((i + i2) - 1) + 1
.=
((i + i2) -' 1) + 1
by A3, NAT_D:37
;
len (mid (h,i2,i1)) = (i1 -' i2) + 1
by A1, A2, A3, A4, A25, FINSEQ_6:118;
then
(i + 1) - 1
<= ((i1 -' i2) + 1) - 1
by A29, XREAL_1:9;
then
i <= i1 - i2
by A25, XREAL_1:233;
then A41:
i + i2 <= (i1 - i2) + i2
by XREAL_1:6;
then A42:
i + i2 <= len h
by A2, XXREAL_0:2;
A43:
i + i2 <= len h
by A2, A41, XXREAL_0:2;
then
h /. ((i + i2) -' 1) = h . ((i + i2) -' 1)
by A36, FINSEQ_4:15, NAT_D:44;
then LSeg (
(mid (h,i2,i1)),
i) =
LSeg (
(h /. ((i + i2) -' 1)),
(h /. (((i + 1) + i2) -' 1)))
by A30, A32, A38, A33, A34, A39, A37, A42, FINSEQ_4:15
.=
LSeg (
h,
((i + i2) -' 1))
by A35, A43, A39, A40, TOPREAL1:def 3
;
then
LSeg (
(mid (h,i2,i1)),
i)
in { (LSeg (h,j)) where j is Nat : ( 1 <= j & j + 1 <= len h ) }
by A35, A39, A40, A42;
then
x in union { (LSeg (h,j)) where j is Nat : ( 1 <= j & j + 1 <= len h ) }
by A26, A27, TARSKI:def 4;
hence
x in L~ h
by TOPREAL1:def 4;
verum end;
hence
x in L~ h
;
verum
end;