let h be FinSequence of (TOP-REAL 2); for i1, i2 being Element of 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 Element of 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
set ;
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 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 Element of NAT : ( 1 <= i & i + 1 <= len (mid h,i1,i2) ) }
by A5, TOPREAL1:def 6;
then consider Y being
set such that A7:
(
x in Y &
Y in { (LSeg (mid h,i1,i2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (mid h,i1,i2) ) } )
by TARSKI:def 4;
consider i being
Element of
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 5;
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:124;
A14:
(mid h,i1,i2) /. i = (mid h,i1,i2) . i
by A9, A12, FINSEQ_4:24;
A15:
(mid h,i1,i2) /. (i + 1) = (mid h,i1,i2) . (i + 1)
by A10, FINSEQ_4:24, NAT_1:11;
1
+ 1
<= i + i1
by A1, A9, XREAL_1:9;
then A16:
(1 + 1) - 1
<= (i + i1) - 1
by XREAL_1:11;
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:124;
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:124;
then
(i + 1) - 1
<= ((i2 -' i1) + 1) - 1
by A10, XREAL_1:11;
then
i <= i2 - i1
by A6, XREAL_1:235;
then A22:
i + i1 <= (i2 - i1) + i1
by XREAL_1:8;
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:24, 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:24
.=
LSeg h,
((i + i1) -' 1)
by A16, A24, A20, A21, TOPREAL1:def 5
;
then
LSeg (mid h,i1,i2),
i in { (LSeg h,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len h ) }
by A16, A20, A21, A23;
then
x in union { (LSeg h,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len h ) }
by A7, A8, TARSKI:def 4;
hence
x in L~ h
by TOPREAL1:def 6;
verum end; case A25:
i1 > i2
;
x in L~ h
mid h,
i1,
i2 = Rev (mid h,i2,i1)
by Th30;
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 Element of NAT : ( 1 <= i & i + 1 <= len (mid h,i2,i1) ) }
by TOPREAL1:def 6;
then consider Y being
set such that A26:
(
x in Y &
Y in { (LSeg (mid h,i2,i1),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (mid h,i2,i1) ) } )
by TARSKI:def 4;
consider i being
Element of
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 5;
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:124;
A33:
(mid h,i2,i1) /. i = (mid h,i2,i1) . i
by A28, A31, FINSEQ_4:24;
A34:
(mid h,i2,i1) /. (i + 1) = (mid h,i2,i1) . (i + 1)
by A29, FINSEQ_4:24, NAT_1:11;
1
+ 1
<= i + i2
by A3, A28, XREAL_1:9;
then A35:
(1 + 1) - 1
<= (i + i2) - 1
by XREAL_1:11;
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:124;
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:124;
then
(i + 1) - 1
<= ((i1 -' i2) + 1) - 1
by A29, XREAL_1:11;
then
i <= i1 - i2
by A25, XREAL_1:235;
then A41:
i + i2 <= (i1 - i2) + i2
by XREAL_1:8;
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:24, 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:24
.=
LSeg h,
((i + i2) -' 1)
by A35, A43, A39, A40, TOPREAL1:def 5
;
then
LSeg (mid h,i2,i1),
i in { (LSeg h,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len h ) }
by A35, A39, A40, A42;
then
x in union { (LSeg h,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len h ) }
by A26, A27, TARSKI:def 4;
hence
x in L~ h
by TOPREAL1:def 6;
verum end;
hence
x in L~ h
;
verum
end;