let f be constant standard special_circular_sequence; for g being FinSequence of (TOP-REAL 2)
for i1, i2 being 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 (TOP-REAL 2); for i1, i2 being 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 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, Th26;
set f1 = mid (f,i1,(len f));
A4:
1 <= i1
by A1;
then A5:
i1 - 1 = i1 -' 1
by XREAL_1:233;
A6:
1 <= len g
by A1;
then A7:
g /. (len g) = g . (len g)
by FINSEQ_4:15;
A8:
len g < len f
by A1;
then A9:
1 < len f
by A6, XXREAL_0:2;
then A10:
f . (len f) = f /. (len f)
by FINSEQ_4:15;
A11:
i1 + 1 <= len f
by A1;
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, FINSEQ_6:188;
A14:
1 <= i2
by A1;
then
1 < i1
by A2, XXREAL_0:2;
then A15:
mid (f,i1,(len f)) is being_S-Seq
by A12, Th40;
A16:
i2 + 1 <= len f
by A1;
then A17:
i2 < len f
by NAT_1:13;
then A18:
(mid (f,1,i2)) . 1 = f . 1
by A14, A9, FINSEQ_6:118;
Z1:
f . 1 = f /. 1
by A9, FINSEQ_4:15;
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, FINSEQ_6:118;
g . (len g) = f . i2
by A1;
then A21:
f /. i2 = g /. (len g)
by A14, A17, A7, FINSEQ_4:15;
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:9;
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:9;
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:15;
(i1 + 1) - i1 <= (len f) - i1
by A11, XREAL_1:9;
then
1 <= (len f) -' i1
by NAT_D:39;
then A25: (((len f) -' i1) -' 1) + 1 =
(((len f) -' i1) - 1) + 1
by XREAL_1:233
.=
(len f) - i1
by A12, XREAL_1:233
;
A26:
L~ (f | i2) = union { (LSeg ((f | i2),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f | i2) ) }
by TOPREAL1:def 4;
A27:
(len f) -' 1 < ((len f) -' 1) + 1
by NAT_1:13;
A28:
(len f) -' 1 = (len f) - 1
by A6, A8, XREAL_1:233, XXREAL_0:2;
then A29:
((len f) -' 1) + 1 = len f
;
A30:
(i1 + 1) - 1 <= (len f) - 1
by A11, XREAL_1:9;
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, FINSEQ_6:118
.=
(((len f) - 1) - i1) + 1
by A28, A30, XREAL_1:233
.=
(len f) - i1
;
len (mid (f,i1,((len f) -' 1))) = (((len f) -' 1) -' i1) + 1
by A4, A28, A12, A30, A31, A27, FINSEQ_6:118;
then
1 <= len (mid (f,i1,((len f) -' 1)))
by NAT_1:11;
then
1 in Seg (len (mid (f,i1,((len f) -' 1))))
;
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, FINSEQ_6:118;
then A33:
f /. i1 = g /. 1
by A6, A24, FINSEQ_4:15;
A34:
L~ (f /^ (i1 -' 1)) = union { (LSeg ((f /^ (i1 -' 1)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) }
by TOPREAL1:def 4;
A35:
f /. 1 = f /. (len f)
by FINSEQ_6:def 1;
A36:
1 + 1 <= len f
by A9, NAT_1:13;
A38:
now ( ( i2 > 1 & (mid ((mid (f,i1,(len f))),1,((len (mid (f,i1,(len f)))) -' 1))) ^ (mid (f,1,i2)) is being_S-Seq ) or ( i2 = 1 & (mid ((mid (f,i1,(len f))),1,((len (mid (f,i1,(len f)))) -' 1))) ^ (mid (f,1,i2)) is being_S-Seq ) )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 Nat : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg ((f | i2),j)) where j is Nat : ( 1 <= j & j + 1 <= len (f | i2) ) } ) = {(f . 1)}
proof
A40:
(f | 2) . (1 + 1) = f . (1 + 1)
by FINSEQ_3:112;
A41:
(f | 2) . 1
= f . 1
by FINSEQ_3:112;
A42:
len (f | 2) = 2
by A36, FINSEQ_1:59;
then A43:
(f | 2) /. 1
= (f | 2) . 1
by FINSEQ_4:15;
(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 3;
A45:
len (f | i2) = i2
by A17, FINSEQ_1:59;
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 3;
(f | i2) . 1
= f . 1
by A14, FINSEQ_3:112;
then A48:
(f | 2) /. 1
= (f | i2) /. 1
by A14, A43, A41, A45, FINSEQ_4:15;
A49:
f . 1
= f /. 1
by A9, FINSEQ_4:15;
A50:
(len (f | 2)) -' 1 =
(1 + 1) -' 1
by A36, FINSEQ_1:59
.=
1
by NAT_D:34
;
then
(f | 2) /. ((len (f | 2)) -' 1) = f /. 1
by A49, A43, FINSEQ_3:112;
then A51:
f . 1
in LSeg (
(f | 2),
((len (f | 2)) -' 1))
by A49, A44, RLTOPSP1:68;
A52:
(f | 2) /. (1 + 1) = (f | 2) . (1 + 1)
by A42, FINSEQ_4:15;
A53:
f /. (len f) in LSeg (
((f /^ (i1 -' 1)) /. ((len (f /^ (i1 -' 1))) -' 1)),
(f /. (len f)))
by RLTOPSP1:68;
(f | i2) . (1 + 1) = f . (1 + 1)
by A45, A46, FINSEQ_3:112;
then A54:
(f | 2) /. (1 + 1) = (f | i2) /. (1 + 1)
by A46, A40, A52, FINSEQ_4:15;
A55:
len (f /^ (i1 -' 1)) = (len f) -' (i1 -' 1)
by RFINSEQ:29;
i1 - i1 < (len f) - i1
by A12, XREAL_1:9;
then
(i1 - i1) + 1
< ((len f) - i1) + 1
by XREAL_1:6;
then
1
< (len f) - (i1 - 1)
;
then
1
< (len f) - (i1 -' 1)
by A4, XREAL_1:233;
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:233
.=
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:9;
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 3;
A60:
LSeg (
(f /^ (i1 -' 1)),
((len (f /^ (i1 -' 1))) -' 1))
in { (LSeg ((f /^ (i1 -' 1)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) }
by A58, A57;
A61:
i1 - 1
< (len f) - 1
by A12, XREAL_1:9;
then
i1 - 1
< len f
by A28, A27, XXREAL_0:2;
then A62:
i1 -' 1
< len f
by A4, XREAL_1:233;
then
(f /^ (i1 -' 1)) /. (((len (f /^ (i1 -' 1))) -' 1) + 1) = f /. (len f)
by A57, FINSEQ_6:185;
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 Nat : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) }
by A60, TARSKI:def 4;
i1 -' 1
<= (len f) - 1
by A4, A61, XREAL_1:233;
then A64:
i1 -' 1
<= (len f) -' 1
by A6, A8, XREAL_1:233, XXREAL_0:2;
A65:
(union { (LSeg ((f /^ (i1 -' 1)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg ((f | i2),j)) where j is Nat : ( 1 <= j & j + 1 <= len (f | i2) ) } ) c= {(f . 1)}
proof
let x be
object ;
TARSKI:def 3 ( not x in (union { (LSeg ((f /^ (i1 -' 1)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg ((f | i2),j)) where j is 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 Nat : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg ((f | i2),j)) where j is Nat : ( 1 <= j & j + 1 <= len (f | i2) ) } )
;
x in {(f . 1)}
then
x in union { (LSeg ((f /^ (i1 -' 1)),i)) where i is 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 Nat : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } )
by TARSKI:def 4;
consider j1 being
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:7;
j1 + 1
<= (len f) -' (i1 -' 1)
by A70, RFINSEQ:29;
then
(j1 + 1) + (i1 -' 1) <= ((len f) -' (i1 -' 1)) + (i1 -' 1)
by XREAL_1:6;
then
(j1 + 1) + (i1 -' 1) <= len f
by A62, XREAL_1:235;
then A72:
(f /^ (i1 -' 1)) . (j1 + 1) = f . (((i1 -' 1) + j1) + 1)
by FINSEQ_6:114, 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:15;
(j1 + 1) + (i1 -' 1) <= ((len f) -' (i1 -' 1)) + (i1 -' 1)
by A55, A70, XREAL_1:6;
then A74:
(j1 + 1) + (i1 -' 1) <= len f
by A62, XREAL_1:235;
A75:
LSeg (
(f /^ (i1 -' 1)),
j1)
= LSeg (
((f /^ (i1 -' 1)) /. j1),
((f /^ (i1 -' 1)) /. (j1 + 1)))
by A69, A70, TOPREAL1:def 3;
A76:
(f /^ (i1 -' 1)) /. (j1 + 1) = (f /^ (i1 -' 1)) . (j1 + 1)
by A70, FINSEQ_4:15, 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, FINSEQ_6:114;
then A78:
(f /^ (i1 -' 1)) /. j1 = f /. ((i1 -' 1) + j1)
by A71, A73, A77, FINSEQ_4:15;
LSeg (
f,
((i1 -' 1) + j1))
= LSeg (
(f /. ((i1 -' 1) + j1)),
(f /. (((i1 -' 1) + j1) + 1)))
by A71, A74, TOPREAL1:def 3;
then A79:
LSeg (
(f /^ (i1 -' 1)),
j1)
= LSeg (
f,
((i1 -' 1) + j1))
by A75, A74, A78, A72, A76, FINSEQ_4:15, NAT_1:11;
x in union { (LSeg ((f | i2),j)) where j is 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 Nat : ( 1 <= i & i + 1 <= len (f | i2) ) } )
by TARSKI:def 4;
consider j2 being
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:16;
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:15, NAT_1:11
.=
f . (j2 + 1)
by A45, A83, FINSEQ_3:112
.=
f /. (j2 + 1)
by A86, FINSEQ_4:15, NAT_1:11
;
A88:
LSeg (
(f | i2),
j2)
= LSeg (
((f | i2) /. j2),
((f | i2) /. (j2 + 1)))
by A82, A83, TOPREAL1:def 3;
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:15
.=
f . j2
by A45, A89, FINSEQ_3:112
.=
f /. j2
by A82, A90, FINSEQ_4:15
;
then A91:
LSeg (
(f | i2),
j2)
= LSeg (
f,
j2)
by A82, A87, A88, A85, TOPREAL1:def 3;
A92:
now ( j2 = 1 & (i1 -' 1) + j1 = (len f) -' 1 )
len (f /^ (i1 -' 1)) = (len f) - (i1 -' 1)
by A12, A55, NAT_D:44, XREAL_1:233;
then A93:
(j1 + 1) + (i1 -' 1) <= ((len f) - (i1 -' 1)) + (i1 -' 1)
by A70, XREAL_1:6;
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:6;
A98:
(i1 -' 1) + 1
= i1
by A4, XREAL_1:235;
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:9;
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:233;
A103:
((((len f) -' 1) -' (i1 -' 1)) + 1) + (i1 -' 1) =
((((len f) -' 1) - (i1 -' 1)) + 1) + (i1 -' 1)
by A64, XREAL_1:233
.=
((len f) -' 1) + 1
.=
((len f) - 1) + 1
by A6, A8, XREAL_1:233, XXREAL_0:2
.=
len f
;
A104:
len (f /^ (i1 -' 1)) = (len f) - (i1 -' 1)
by A12, A55, NAT_D:44, XREAL_1:233;
((len f) -' 1) - (i1 -' 1) < (len f) - (i1 -' 1)
by A28, A27, XREAL_1:9;
then A105:
((len f) -' 1) -' (i1 -' 1) < len (f /^ (i1 -' 1))
by A64, A104, XREAL_1:233;
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:9;
then A107:
i1 - (i1 - 1) <= ((len f) - 1) - (i1 - 1)
by XREAL_1:9;
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:15
.=
f . ((((len f) -' 1) -' (i1 -' 1)) + (i1 -' 1))
by A102, A108, FINSEQ_6:114
.=
f . ((((len f) -' 1) - (i1 -' 1)) + (i1 -' 1))
by A64, XREAL_1:233
.=
f /. ((len f) -' 1)
by A28, A31, A27, FINSEQ_4:15
;
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:15
.=
f . (1 + ((((len f) -' 1) -' (i1 -' 1)) + (i1 -' 1)))
by A103, A110, FINSEQ_6:114
.=
f . (((((len f) -' 1) - (i1 -' 1)) + (i1 -' 1)) + 1)
by A64, XREAL_1:233
.=
f . (len f)
by A6, A8, XREAL_1:235, XXREAL_0:2
.=
f /. (len f)
by A9, FINSEQ_4:15
;
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:233
;
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 3
.=
LSeg (
f,
((len f) -' 1))
by A29, A31, A109, A111, TOPREAL1:def 3
;
then
(LSeg ((f /^ (i1 -' 1)),j1)) /\ (LSeg ((f | i2),j2)) = {(f . 1)}
by A101, Th42;
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 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 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 Nat : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg ((f | i2),j)) where j is 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 Nat : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg ((f | i2),j)) where j is Nat : ( 1 <= j & j + 1 <= len (f | i2) ) } )
by ZFMISC_1:31;
hence
(union { (LSeg ((f /^ (i1 -' 1)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg ((f | i2),j)) where j is 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, FINSEQ_6:116;
then A113:
(L~ (mid (f,i1,(len f)))) /\ (L~ (mid (f,1,i2))) = {((mid (f,1,i2)) . 1)}
by A12, A18, FINSEQ_6:117;
mid (
f,1,
i2) is
being_S-Seq
by A16, A39, Th39;
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:45;
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 FINSEQ_6:116
.=
<*(f . 1)*>
by FINSEQ_5:20
;
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, FINSEQ_6:116;
A116:
((len (mid (f,i1,(len f)))) -' 1) + 1
= len (mid (f,i1,(len f)))
by A20, NAT_D:34;
1
<= len (mid (f,i1,(len f)))
by A20, NAT_1:11;
then
len (mid (f,i1,(len f))) in dom (mid (f,i1,(len f)))
by FINSEQ_3:25;
then Z:
(mid (f,i1,(len f))) /. (len (mid (f,i1,(len f)))) = (mid (f,i1,(len f))) . (len (mid (f,i1,(len f))))
by PARTFUN1:def 6;
<*(f . 1)*> = <*((mid (f,i1,(len f))) . (len (mid (f,i1,(len f)))))*>
by Z1, A13, A10, A35;
hence
(mid ((mid (f,i1,(len f))),1,((len (mid (f,i1,(len f)))) -' 1))) ^ (mid (f,1,i2)) is
being_S-Seq
by Z, A15, A114, A115, A116, FINSEQ_5:21;
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, FINSEQ_6:118
.=
(((((len f) -' i1) + 1) -' 1) -' 1) + 1
by A4, A9, A12, FINSEQ_6:118
;
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, FINSEQ_6:118;
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:233;
then A122:
k < len (mid (f,i1,(len f)))
by A119, NAT_1:13;
(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, FINSEQ_6:118
.=
(mid (f,i1,(len f))) . k
by NAT_D:34
.=
f . ((k + i1) -' 1)
by A4, A9, A12, A120, A122, FINSEQ_6:118
;
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, FINSEQ_6:118;
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:14;
then
g is being_S-Seq
by A1, A2, A38, Th26;
hence
L~ g is_S-P_arc_joining f /. i1,f /. i2
by A33, A21, TOPREAL4:def 1; verum