let f be non constant standard special_circular_sequence; for g being FinSequence of
for i1, i2 being Element of NAT st g is_a_part>_of f,i1,i2 & i1 > i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2
let g be FinSequence of ; for i1, i2 being Element of NAT st g is_a_part>_of f,i1,i2 & i1 > i2 holds
L~ g is_S-P_arc_joining f /. i1,f /. i2
let i1, i2 be Element of NAT ; ( g is_a_part>_of f,i1,i2 & i1 > i2 implies L~ g is_S-P_arc_joining f /. i1,f /. i2 )
assume that
A1:
g is_a_part>_of f,i1,i2
and
A2:
i1 > i2
; L~ g is_S-P_arc_joining f /. i1,f /. i2
A3:
g = (mid f,i1,((len f) -' 1)) ^ (f | i2)
by A1, A2, Th38;
set f1 = mid f,i1,(len f);
A4:
1 <= i1
by A1, Def2;
then A5:
i1 - 1 = i1 -' 1
by XREAL_1:235;
A6:
1 <= len g
by A1, Def2;
then A7:
g /. (len g) = g . (len g)
by FINSEQ_4:24;
A8:
len g < len f
by A1, Def2;
then A9:
1 < len f
by A6, XXREAL_0:2;
then A10:
f . (len f) = f /. (len f)
by FINSEQ_4:24;
A11:
i1 + 1 <= len f
by A1, Def2;
then A12:
i1 < len f
by NAT_1:13;
then A13:
(mid f,i1,(len f)) . (len (mid f,i1,(len f))) = f . (len f)
by A4, Th22;
A14:
1 <= i2
by A1, Def2;
then
1 < i1
by A2, XXREAL_0:2;
then A15:
mid f,i1,(len f) is being_S-Seq
by A12, Th52;
A16:
i2 + 1 <= len f
by A1, Def2;
then A17:
i2 < len f
by NAT_1:13;
then A18:
(mid f,1,i2) . 1 = f . 1
by A14, A9, JORDAN3:27;
f . 1 = f /. 1
by A9, FINSEQ_4:24;
then A19:
(mid f,i1,(len f)) . (len (mid f,i1,(len f))) = (mid f,1,i2) . 1
by A13, A18, A10, FINSEQ_6:def 1;
A20:
len (mid f,i1,(len f)) = ((len f) -' i1) + 1
by A4, A9, A12, JORDAN3:27;
g . (len g) = f . i2
by A1, Def2;
then A21:
f /. i2 = g /. (len g)
by A14, A17, A7, FINSEQ_4:24;
len (mid f,i1,(len f)) < (len (mid f,i1,(len f))) + 1
by NAT_1:13;
then
(len (mid f,i1,(len f))) - 1 < ((len (mid f,i1,(len f))) + 1) - 1
by XREAL_1:11;
then A22:
(len (mid f,i1,(len f))) -' 1 <= len (mid f,i1,(len f))
by A20, NAT_D:34;
(i1 + 1) - i1 <= (len f) - i1
by A11, XREAL_1:11;
then
1 <= (len f) -' i1
by NAT_D:39;
then A23:
1 <= (len (mid f,i1,(len f))) -' 1
by A20, NAT_D:34;
i1 < len f
by A11, NAT_1:13;
then A24:
f /. i1 = f . i1
by A4, FINSEQ_4:24;
(i1 + 1) - i1 <= (len f) - i1
by A11, XREAL_1:11;
then
1 <= (len f) -' i1
by NAT_D:39;
then A25: (((len f) -' i1) -' 1) + 1 =
(((len f) -' i1) - 1) + 1
by XREAL_1:235
.=
(len f) - i1
by A12, XREAL_1:235
;
A26:
L~ (f | i2) = union { (LSeg (f | i2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f | i2) ) }
by TOPREAL1:def 6;
A27:
(len f) -' 1 < ((len f) -' 1) + 1
by NAT_1:13;
A28:
(len f) -' 1 = (len f) - 1
by A6, A8, XREAL_1:235, XXREAL_0:2;
then A29:
((len f) -' 1) + 1 = len f
;
A30:
(i1 + 1) - 1 <= (len f) - 1
by A11, XREAL_1:11;
then A31:
1 <= (len f) -' 1
by A4, A28, XXREAL_0:2;
then A32: len (mid f,i1,((len f) -' 1)) =
(((len f) -' 1) -' i1) + 1
by A4, A28, A12, A30, A27, JORDAN3:27
.=
(((len f) - 1) - i1) + 1
by A28, A30, XREAL_1:235
.=
(len f) - i1
;
len (mid f,i1,((len f) -' 1)) = (((len f) -' 1) -' i1) + 1
by A4, A28, A12, A30, A31, A27, JORDAN3:27;
then
1 <= len (mid f,i1,((len f) -' 1))
by NAT_1:11;
then
1 in Seg (len (mid f,i1,((len f) -' 1)))
by FINSEQ_1:3;
then
1 in dom (mid f,i1,((len f) -' 1))
by FINSEQ_1:def 3;
then
g . 1 = (mid f,i1,((len f) -' 1)) . 1
by A3, FINSEQ_1:def 7;
then
g . 1 = f . i1
by A4, A28, A12, A31, A27, JORDAN3:27;
then A33:
f /. i1 = g /. 1
by A6, A24, FINSEQ_4:24;
A34:
L~ (f /^ (i1 -' 1)) = union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) }
by TOPREAL1:def 6;
A35:
f /. 1 = f /. (len f)
by FINSEQ_6:def 1;
A36:
1 + 1 <= len f
by A9, NAT_1:13;
A37:
1 <= len (mid f,i1,(len f))
by A20, NAT_1:11;
A38:
now per cases
( i2 > 1 or i2 = 1 )
by A14, XXREAL_0:1;
case A39:
i2 > 1
;
(mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) ^ (mid f,1,i2) is being_S-Seq
(union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) } ) = {(f . 1)}
proof
A40:
(f | 2) . (1 + 1) = f . (1 + 1)
by FINSEQ_3:121;
A41:
(f | 2) . 1
= f . 1
by FINSEQ_3:121;
A42:
len (f | 2) = 2
by A36, FINSEQ_1:80;
then A43:
(f | 2) /. 1
= (f | 2) . 1
by FINSEQ_4:24;
(len (f | 2)) -' 1 =
2
- 1
by A42, NAT_D:39
.=
1
;
then A44:
LSeg (f | 2),
((len (f | 2)) -' 1) = LSeg ((f | 2) /. ((len (f | 2)) -' 1)),
((f | 2) /. (((len (f | 2)) -' 1) + 1))
by A42, TOPREAL1:def 5;
A45:
len (f | i2) = i2
by A17, FINSEQ_1:80;
then A46:
1
+ 1
<= len (f | i2)
by A39, NAT_1:13;
then A47:
LSeg (f | i2),1
= LSeg ((f | i2) /. 1),
((f | i2) /. (1 + 1))
by TOPREAL1:def 5;
(f | i2) . 1
= f . 1
by A14, FINSEQ_3:121;
then A48:
(f | 2) /. 1
= (f | i2) /. 1
by A14, A43, A41, A45, FINSEQ_4:24;
A49:
f . 1
= f /. 1
by A9, FINSEQ_4:24;
A50:
(len (f | 2)) -' 1 =
(1 + 1) -' 1
by A36, FINSEQ_1:80
.=
1
by NAT_D:34
;
then
(f | 2) /. ((len (f | 2)) -' 1) = f /. 1
by A49, A43, FINSEQ_3:121;
then A51:
f . 1
in LSeg (f | 2),
((len (f | 2)) -' 1)
by A49, A44, RLTOPSP1:69;
A52:
(f | 2) /. (1 + 1) = (f | 2) . (1 + 1)
by A42, FINSEQ_4:24;
A53:
f /. (len f) in LSeg ((f /^ (i1 -' 1)) /. ((len (f /^ (i1 -' 1))) -' 1)),
(f /. (len f))
by RLTOPSP1:69;
(f | i2) . (1 + 1) = f . (1 + 1)
by A45, A46, FINSEQ_3:121;
then A54:
(f | 2) /. (1 + 1) = (f | i2) /. (1 + 1)
by A46, A40, A52, FINSEQ_4:24;
A55:
len (f /^ (i1 -' 1)) = (len f) -' (i1 -' 1)
by JORDAN3:19;
i1 - i1 < (len f) - i1
by A12, XREAL_1:11;
then
(i1 - i1) + 1
< ((len f) - i1) + 1
by XREAL_1:8;
then
1
< (len f) - (i1 - 1)
;
then
1
< (len f) - (i1 -' 1)
by A4, XREAL_1:235;
then A56:
1
< len (f /^ (i1 -' 1))
by A55, NAT_D:39;
then A57:
((len (f /^ (i1 -' 1))) -' 1) + 1 =
((len (f /^ (i1 -' 1))) - 1) + 1
by XREAL_1:235
.=
len (f /^ (i1 -' 1))
;
1
+ 1
<= len (f /^ (i1 -' 1))
by A56, NAT_1:13;
then A58:
(1 + 1) - 1
<= (len (f /^ (i1 -' 1))) - 1
by XREAL_1:11;
then A59:
LSeg (f /^ (i1 -' 1)),
((len (f /^ (i1 -' 1))) -' 1) = LSeg ((f /^ (i1 -' 1)) /. ((len (f /^ (i1 -' 1))) -' 1)),
((f /^ (i1 -' 1)) /. (((len (f /^ (i1 -' 1))) -' 1) + 1))
by A57, TOPREAL1:def 5;
A60:
LSeg (f /^ (i1 -' 1)),
((len (f /^ (i1 -' 1))) -' 1) in { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) }
by A58, A57;
A61:
i1 - 1
< (len f) - 1
by A12, XREAL_1:11;
then
i1 - 1
< len f
by A28, A27, XXREAL_0:2;
then A62:
i1 -' 1
< len f
by A4, XREAL_1:235;
then
(f /^ (i1 -' 1)) /. (((len (f /^ (i1 -' 1))) -' 1) + 1) = f /. (len f)
by A57, Th18;
then
f . 1
in LSeg (f /^ (i1 -' 1)),
((len (f /^ (i1 -' 1))) -' 1)
by A59, A53, A49, FINSEQ_6:def 1;
then A63:
f . 1
in union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) }
by A60, TARSKI:def 4;
i1 -' 1
<= (len f) - 1
by A4, A61, XREAL_1:235;
then A64:
i1 -' 1
<= (len f) -' 1
by A6, A8, XREAL_1:235, XXREAL_0:2;
A65:
(union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) } ) c= {(f . 1)}
proof
let x be
set ;
TARSKI:def 3 ( not x in (union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) } ) or x in {(f . 1)} )
assume A66:
x in (union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) } )
;
x in {(f . 1)}
then
x in union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) }
by XBOOLE_0:def 4;
then consider Y1 being
set such that A67:
(
x in Y1 &
Y1 in { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } )
by TARSKI:def 4;
consider j1 being
Element of
NAT such that A68:
Y1 = LSeg (f /^ (i1 -' 1)),
j1
and A69:
1
<= j1
and A70:
j1 + 1
<= len (f /^ (i1 -' 1))
by A67;
A71:
0 + 1
<= (i1 -' 1) + j1
by A69, XREAL_1:9;
j1 + 1
<= (len f) -' (i1 -' 1)
by A70, JORDAN3:19;
then
(j1 + 1) + (i1 -' 1) <= ((len f) -' (i1 -' 1)) + (i1 -' 1)
by XREAL_1:8;
then
(j1 + 1) + (i1 -' 1) <= len f
by A62, XREAL_1:237;
then A72:
(f /^ (i1 -' 1)) . (j1 + 1) = f . (((i1 -' 1) + j1) + 1)
by JORDAN3:23, NAT_1:11;
j1 <= len (f /^ (i1 -' 1))
by A70, NAT_1:13;
then A73:
(f /^ (i1 -' 1)) /. j1 = (f /^ (i1 -' 1)) . j1
by A69, FINSEQ_4:24;
(j1 + 1) + (i1 -' 1) <= ((len f) -' (i1 -' 1)) + (i1 -' 1)
by A55, A70, XREAL_1:8;
then A74:
(j1 + 1) + (i1 -' 1) <= len f
by A62, XREAL_1:237;
A75:
LSeg (f /^ (i1 -' 1)),
j1 = LSeg ((f /^ (i1 -' 1)) /. j1),
((f /^ (i1 -' 1)) /. (j1 + 1))
by A69, A70, TOPREAL1:def 5;
A76:
(f /^ (i1 -' 1)) /. (j1 + 1) = (f /^ (i1 -' 1)) . (j1 + 1)
by A70, FINSEQ_4:24, NAT_1:11;
(i1 -' 1) + j1 <= ((i1 -' 1) + j1) + 1
by NAT_1:11;
then A77:
j1 + (i1 -' 1) <= len f
by A74, XXREAL_0:2;
then
(f /^ (i1 -' 1)) . j1 = f . ((i1 -' 1) + j1)
by A69, JORDAN3:23;
then A78:
(f /^ (i1 -' 1)) /. j1 = f /. ((i1 -' 1) + j1)
by A71, A73, A77, FINSEQ_4:24;
LSeg f,
((i1 -' 1) + j1) = LSeg (f /. ((i1 -' 1) + j1)),
(f /. (((i1 -' 1) + j1) + 1))
by A71, A74, TOPREAL1:def 5;
then A79:
LSeg (f /^ (i1 -' 1)),
j1 = LSeg f,
((i1 -' 1) + j1)
by A75, A74, A78, A72, A76, FINSEQ_4:24, NAT_1:11;
x in union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) }
by A66, XBOOLE_0:def 4;
then consider Y2 being
set such that A80:
(
x in Y2 &
Y2 in { (LSeg (f | i2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f | i2) ) } )
by TARSKI:def 4;
consider j2 being
Element of
NAT such that A81:
Y2 = LSeg (f | i2),
j2
and A82:
1
<= j2
and A83:
j2 + 1
<= len (f | i2)
by A80;
A84:
len (f | i2) <= len f
by FINSEQ_5:18;
then A85:
j2 + 1
<= len f
by A83, XXREAL_0:2;
A86:
j2 + 1
<= len f
by A83, A84, XXREAL_0:2;
A87:
(f | i2) /. (j2 + 1) =
(f | i2) . (j2 + 1)
by A83, FINSEQ_4:24, NAT_1:11
.=
f . (j2 + 1)
by A45, A83, FINSEQ_3:121
.=
f /. (j2 + 1)
by A86, FINSEQ_4:24, NAT_1:11
;
A88:
LSeg (f | i2),
j2 = LSeg ((f | i2) /. j2),
((f | i2) /. (j2 + 1))
by A82, A83, TOPREAL1:def 5;
A89:
j2 < len (f | i2)
by A83, NAT_1:13;
then A90:
j2 < len f
by A84, XXREAL_0:2;
(f | i2) /. j2 =
(f | i2) . j2
by A82, A89, FINSEQ_4:24
.=
f . j2
by A45, A89, FINSEQ_3:121
.=
f /. j2
by A82, A90, FINSEQ_4:24
;
then A91:
LSeg (f | i2),
j2 = LSeg f,
j2
by A82, A87, A88, A85, TOPREAL1:def 5;
A92:
now
len (f /^ (i1 -' 1)) = (len f) - (i1 -' 1)
by A12, A55, NAT_D:44, XREAL_1:235;
then A93:
(j1 + 1) + (i1 -' 1) <= ((len f) - (i1 -' 1)) + (i1 -' 1)
by A70, XREAL_1:8;
then
((i1 -' 1) + j1) + 1
<= len f
;
then A94:
(i1 -' 1) + j1 < len f
by NAT_1:13;
A95:
i2 + 1
<= i1
by A2, NAT_1:13;
assume A96:
( not
j2 = 1 or not
(i1 -' 1) + j1 = (len f) -' 1 )
;
contradictionA97:
(i1 -' 1) + 1
<= (i1 -' 1) + j1
by A69, XREAL_1:8;
A98:
(i1 -' 1) + 1
= i1
by A4, XREAL_1:237;
j2 + 1
< i2 + 1
by A45, A83, NAT_1:13;
then
j2 + 1
< (i1 -' 1) + 1
by A95, A98, XXREAL_0:2;
then A99:
j2 + 1
< (i1 -' 1) + j1
by A97, XXREAL_0:2;
A100:
(((i1 -' 1) + j1) + 1) - 1
<= (len f) - 1
by A93, XREAL_1:11;
hence
contradiction
by A67, A68, A80, A81, A79, A91, XBOOLE_0:def 4;
verum end;
then A101:
LSeg (f | i2),
j2 = LSeg f,1
by A46, SPPOL_2:3;
(((len f) -' 1) - (i1 -' 1)) + (i1 -' 1) <= len f
by A28, A27;
then A102:
(((len f) -' 1) -' (i1 -' 1)) + (i1 -' 1) <= len f
by A64, XREAL_1:235;
A103:
((((len f) -' 1) -' (i1 -' 1)) + 1) + (i1 -' 1) =
((((len f) -' 1) - (i1 -' 1)) + 1) + (i1 -' 1)
by A64, XREAL_1:235
.=
((len f) -' 1) + 1
.=
((len f) - 1) + 1
by A6, A8, XREAL_1:235, XXREAL_0:2
.=
len f
;
A104:
len (f /^ (i1 -' 1)) = (len f) - (i1 -' 1)
by A12, A55, NAT_D:44, XREAL_1:235;
((len f) -' 1) - (i1 -' 1) < (len f) - (i1 -' 1)
by A28, A27, XREAL_1:11;
then A105:
((len f) -' 1) -' (i1 -' 1) < len (f /^ (i1 -' 1))
by A64, A104, XREAL_1:235;
then A106:
(((len f) -' 1) -' (i1 -' 1)) + 1
<= len (f /^ (i1 -' 1))
by NAT_1:13;
(i1 + 1) - 1
<= (len f) - 1
by A11, XREAL_1:11;
then A107:
i1 - (i1 - 1) <= ((len f) - 1) - (i1 - 1)
by XREAL_1:11;
then A108:
1
<= ((len f) -' 1) -' (i1 -' 1)
by A28, A5, NAT_D:39;
then A109:
(f /^ (i1 -' 1)) /. (((len f) -' 1) -' (i1 -' 1)) =
(f /^ (i1 -' 1)) . (((len f) -' 1) -' (i1 -' 1))
by A105, FINSEQ_4:24
.=
f . ((((len f) -' 1) -' (i1 -' 1)) + (i1 -' 1))
by A102, A108, JORDAN3:23
.=
f . ((((len f) -' 1) - (i1 -' 1)) + (i1 -' 1))
by A64, XREAL_1:235
.=
f /. ((len f) -' 1)
by A28, A31, A27, FINSEQ_4:24
;
A110:
1
< (((len f) -' 1) -' (i1 -' 1)) + 1
by A108, NAT_1:13;
then A111:
(f /^ (i1 -' 1)) /. ((((len f) -' 1) -' (i1 -' 1)) + 1) =
(f /^ (i1 -' 1)) . ((((len f) -' 1) -' (i1 -' 1)) + 1)
by A106, FINSEQ_4:24
.=
f . (1 + ((((len f) -' 1) -' (i1 -' 1)) + (i1 -' 1)))
by A103, A110, JORDAN3:23
.=
f . (((((len f) -' 1) - (i1 -' 1)) + (i1 -' 1)) + 1)
by A64, XREAL_1:235
.=
f . (len f)
by A6, A8, XREAL_1:237, XXREAL_0:2
.=
f /. (len f)
by A9, FINSEQ_4:24
;
A112:
1
<= ((len f) -' 1) -' (i1 -' 1)
by A28, A5, A107, NAT_D:39;
j1 =
((len f) -' 1) - (i1 -' 1)
by A92
.=
((len f) -' 1) -' (i1 -' 1)
by A64, XREAL_1:235
;
then LSeg (f /^ (i1 -' 1)),
j1 =
LSeg ((f /^ (i1 -' 1)) /. (((len f) -' 1) -' (i1 -' 1))),
((f /^ (i1 -' 1)) /. ((((len f) -' 1) -' (i1 -' 1)) + 1))
by A112, A106, TOPREAL1:def 5
.=
LSeg f,
((len f) -' 1)
by A29, A31, A109, A111, TOPREAL1:def 5
;
then
(LSeg (f /^ (i1 -' 1)),j1) /\ (LSeg (f | i2),j2) = {(f . 1)}
by A101, Th54;
hence
x in {(f . 1)}
by A67, A68, A80, A81, XBOOLE_0:def 4;
verum
end;
1
+ 1
<= len (f | i2)
by A39, A45, NAT_1:13;
then
LSeg (f | 2),
((len (f | 2)) -' 1) in { (LSeg (f | i2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f | i2) ) }
by A44, A50, A48, A54, A47;
then
f . 1
in union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) }
by A51, TARSKI:def 4;
then
f . 1
in (union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) } )
by A63, XBOOLE_0:def 4;
then
{(f . 1)} c= (union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) } )
by ZFMISC_1:37;
hence
(union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) } ) = {(f . 1)}
by A65, XBOOLE_0:def 10;
verum
end; then
(L~ (f /^ (i1 -' 1))) /\ (L~ (mid f,1,i2)) = {(f . 1)}
by A14, A34, A26, JORDAN3:25;
then A113:
(L~ (mid f,i1,(len f))) /\ (L~ (mid f,1,i2)) = {((mid f,1,i2) . 1)}
by A12, A18, JORDAN3:26;
mid f,1,
i2 is
being_S-Seq
by A16, A39, Th51;
hence
(mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) ^ (mid f,1,i2) is
being_S-Seq
by A15, A19, A113, JORDAN3:80;
verum end; case
i2 = 1
;
(mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) ^ (mid f,1,i2) is being_S-Seq then A114:
mid f,1,
i2 =
f | 1
by JORDAN3:25
.=
<*(f /. 1)*>
by FINSEQ_5:23
;
A115:
mid (mid f,i1,(len f)),1,
((len (mid f,i1,(len f))) -' 1) = (mid f,i1,(len f)) | ((len (mid f,i1,(len f))) -' 1)
by A23, JORDAN3:25;
A116:
((len (mid f,i1,(len f))) -' 1) + 1
= len (mid f,i1,(len f))
by A20, NAT_D:34;
<*(f /. 1)*> = <*((mid f,i1,(len f)) /. (len (mid f,i1,(len f))))*>
by A13, A10, A35, A37, FINSEQ_4:24;
hence
(mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) ^ (mid f,1,i2) is
being_S-Seq
by A15, A114, A115, A116, FINSEQ_5:24;
verum end;
A117:
1 <= len (mid f,i1,(len f))
by A20, NAT_1:11;
then len (mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) =
(((len (mid f,i1,(len f))) -' 1) -' 1) + 1
by A23, A22, JORDAN3:27
.=
(((((len f) -' i1) + 1) -' 1) -' 1) + 1
by A4, A9, A12, JORDAN3:27
;
then A118:
len (mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) = len (mid f,i1,((len f) -' 1))
by A25, A32, NAT_D:34;
for k being Nat st 1 <= k & k <= len (mid f,i1,((len f) -' 1)) holds
(mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) . k = (mid f,i1,((len f) -' 1)) . k
proof
A119:
len (mid f,i1,(len f)) = ((len f) -' i1) + 1
by A4, A9, A12, JORDAN3:27;
let k be
Nat;
( 1 <= k & k <= len (mid f,i1,((len f) -' 1)) implies (mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) . k = (mid f,i1,((len f) -' 1)) . k )
assume that A120:
1
<= k
and A121:
k <= len (mid f,i1,((len f) -' 1))
;
(mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) . k = (mid f,i1,((len f) -' 1)) . k
k <= (len f) -' i1
by A12, A32, A121, XREAL_1:235;
then A122:
k < len (mid f,i1,(len f))
by A119, NAT_1:13;
A123:
k in NAT
by ORDINAL1:def 13;
then (mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) . k =
(mid f,i1,(len f)) . ((k + 1) -' 1)
by A117, A23, A22, A118, A120, A121, JORDAN3:27
.=
(mid f,i1,(len f)) . k
by NAT_D:34
.=
f . ((k + i1) -' 1)
by A4, A9, A12, A120, A123, A122, JORDAN3:27
;
hence
(mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) . k = (mid f,i1,((len f) -' 1)) . k
by A4, A28, A12, A30, A31, A27, A120, A121, A123, JORDAN3:27;
verum
end;
then
mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1) = mid f,i1,((len f) -' 1)
by A118, FINSEQ_1:18;
then
g is being_S-Seq
by A1, A2, A38, Th38;
hence
L~ g is_S-P_arc_joining f /. i1,f /. i2
by A33, A21, TOPREAL4:def 1; verum