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;
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 A12:
i + i1 <= (i2 - i1) + i1
by XREAL_1:6;
then A13:
i + i1 <= len h
by A4, XXREAL_0:2;
1
+ 1
<= i + i1
by A1, A9, XREAL_1:7;
then A14:
(1 + 1) - 1
<= (i + i1) - 1
by XREAL_1:9;
then
1
<= (i + i1) -' 1
by A1, NAT_1:12, XREAL_1:233;
then A15:
h /. ((i + i1) -' 1) = h . ((i + i1) -' 1)
by A13, FINSEQ_4:15, NAT_D:44;
1
<= i + 1
by NAT_1:11;
then A16:
(mid (h,i1,i2)) . (i + 1) = h . (((i + 1) + i1) -' 1)
by A1, A2, A3, A4, A6, A10, FINSEQ_6:118;
A17:
((i + 1) + i1) -' 1 =
((i + 1) + i1) - 1
by A1, NAT_1:12, XREAL_1:233
.=
i + i1
;
then A18:
((i + 1) + i1) -' 1 =
((i + i1) - 1) + 1
.=
((i + i1) -' 1) + 1
by A1, NAT_1:12, XREAL_1:233
;
i <= i + 1
by NAT_1:11;
then A19:
i <= len (mid (h,i1,i2))
by A10, XXREAL_0:2;
then A20:
(mid (h,i1,i2)) /. i = (mid (h,i1,i2)) . i
by A9, FINSEQ_4:15;
A21:
(mid (h,i1,i2)) /. (i + 1) = (mid (h,i1,i2)) . (i + 1)
by A10, FINSEQ_4:15, NAT_1:11;
A22:
i + i1 <= len h
by A4, A12, XXREAL_0:2;
(mid (h,i1,i2)) . i = h . ((i + i1) -' 1)
by A1, A2, A3, A4, A6, A9, A19, FINSEQ_6:118;
then LSeg (
(mid (h,i1,i2)),
i) =
LSeg (
(h /. ((i + i1) -' 1)),
(h /. (((i + 1) + i1) -' 1)))
by A1, A11, A16, A20, A21, A15, A17, A22, FINSEQ_4:15, NAT_1:12
.=
LSeg (
h,
((i + i1) -' 1))
by A14, A13, A17, A18, 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 A14, A17, A18, A22;
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 A23:
i1 > i2
;
x in L~ h
mid (
h,
i1,
i2)
= Rev (mid (h,i2,i1))
by Lm6;
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 A24:
(
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 A25:
Y = LSeg (
(mid (h,i2,i1)),
i)
and A26:
1
<= i
and A27:
i + 1
<= len (mid (h,i2,i1))
by A24;
A28:
LSeg (
(mid (h,i2,i1)),
i)
= LSeg (
((mid (h,i2,i1)) /. i),
((mid (h,i2,i1)) /. (i + 1)))
by A26, A27, TOPREAL1:def 3;
len (mid (h,i2,i1)) = (i1 -' i2) + 1
by A1, A2, A3, A4, A23, FINSEQ_6:118;
then
(i + 1) - 1
<= ((i1 -' i2) + 1) - 1
by A27, XREAL_1:9;
then
i <= i1 - i2
by A23, XREAL_1:233;
then A29:
i + i2 <= (i1 - i2) + i2
by XREAL_1:6;
then A30:
i + i2 <= len h
by A2, XXREAL_0:2;
1
+ 1
<= i + i2
by A3, A26, XREAL_1:7;
then A31:
(1 + 1) - 1
<= (i + i2) - 1
by XREAL_1:9;
then
1
<= (i + i2) -' 1
by A3, NAT_1:12, XREAL_1:233;
then A32:
h /. ((i + i2) -' 1) = h . ((i + i2) -' 1)
by A30, FINSEQ_4:15, NAT_D:44;
1
<= i + 1
by NAT_1:11;
then A33:
(mid (h,i2,i1)) . (i + 1) = h . (((i + 1) + i2) -' 1)
by A1, A2, A3, A4, A23, A27, FINSEQ_6:118;
A34:
((i + 1) + i2) -' 1 =
((i + 1) + i2) - 1
by A3, NAT_1:12, XREAL_1:233
.=
i + i2
;
then A35:
((i + 1) + i2) -' 1 =
((i + i2) - 1) + 1
.=
((i + i2) -' 1) + 1
by A3, NAT_1:12, XREAL_1:233
;
i <= i + 1
by NAT_1:11;
then A36:
i <= len (mid (h,i2,i1))
by A27, XXREAL_0:2;
then A37:
(mid (h,i2,i1)) /. i = (mid (h,i2,i1)) . i
by A26, FINSEQ_4:15;
A38:
(mid (h,i2,i1)) /. (i + 1) = (mid (h,i2,i1)) . (i + 1)
by A27, FINSEQ_4:15, NAT_1:11;
A39:
i + i2 <= len h
by A2, A29, XXREAL_0:2;
(mid (h,i2,i1)) . i = h . ((i + i2) -' 1)
by A1, A2, A3, A4, A23, A26, A36, FINSEQ_6:118;
then LSeg (
(mid (h,i2,i1)),
i) =
LSeg (
(h /. ((i + i2) -' 1)),
(h /. (((i + 1) + i2) -' 1)))
by A3, A28, A33, A37, A38, A32, A34, A39, FINSEQ_4:15, NAT_1:12
.=
LSeg (
h,
((i + i2) -' 1))
by A31, A30, A34, A35, 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 A31, A34, A35, A39;
then
x in union { (LSeg (h,j)) where j is Nat : ( 1 <= j & j + 1 <= len h ) }
by A24, A25, TARSKI:def 4;
hence
x in L~ h
by TOPREAL1:def 4;
verum end;
hence
x in L~ h
;
verum
end;