let f be non constant standard special_circular_sequence; for i1, i2 being Element of NAT st 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & i1 <> i2 holds
ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) )
let i1, i2 be Element of NAT ; ( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & i1 <> i2 implies ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) ) )
assume that
A1:
1 <= i1
and
A2:
i1 + 1 <= len f
and
A3:
1 <= i2
and
A4:
i2 + 1 <= len f
and
A5:
i1 <> i2
; ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) )
now per cases
( i1 <= i2 or i1 > i2 )
;
case A6:
i1 <= i2
;
ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) )set h1 =
mid (
f,
i1,
i2);
set h2 =
(mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2));
A7:
i2 < len f
by A4, NAT_1:13;
then A8:
mid (
f,
i1,
i2)
is_a_part>_of f,
i1,
i2
by A1, A6, Th43;
then A9:
mid (
f,
i1,
i2)
is_a_part_of f,
i1,
i2
by Def4;
A10:
i1 < i2
by A5, A6, XXREAL_0:1;
then A11:
L~ (mid (f,i1,i2)) is_S-P_arc_joining f /. i1,
f /. i2
by A8, Th56;
A12:
for
g being
FinSequence of
(TOP-REAL 2) holds
( not
g is_a_part_of f,
i1,
i2 or
g = mid (
f,
i1,
i2) or
g = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) )
proof
let g be
FinSequence of
(TOP-REAL 2);
( not g is_a_part_of f,i1,i2 or g = mid (f,i1,i2) or g = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) )
assume A13:
g is_a_part_of f,
i1,
i2
;
( g = mid (f,i1,i2) or g = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) )
hence
(
g = mid (
f,
i1,
i2) or
g = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) )
;
verum
end; A14:
(L~ (mid (f,i1,i2))) \/ (L~ ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)))) = L~ f
by A1, A10, A7, Th55;
A15:
(L~ (mid (f,i1,i2))) /\ (L~ ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)))) = {(f . i1),(f . i2)}
by A1, A10, A7, Th55;
(mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part<_of f,
i1,
i2
by A1, A10, A7, Th46;
then A16:
(mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part_of f,
i1,
i2
by Def4;
then
L~ ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) is_S-P_arc_joining f /. i1,
f /. i2
by A5, Th60;
hence
ex
g1,
g2 being
FinSequence of
(TOP-REAL 2) st
(
g1 is_a_part_of f,
i1,
i2 &
g2 is_a_part_of f,
i1,
i2 &
(L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} &
(L~ g1) \/ (L~ g2) = L~ f &
L~ g1 is_S-P_arc_joining f /. i1,
f /. i2 &
L~ g2 is_S-P_arc_joining f /. i1,
f /. i2 & ( for
g being
FinSequence of
(TOP-REAL 2) holds
( not
g is_a_part_of f,
i1,
i2 or
g = g1 or
g = g2 ) ) )
by A9, A16, A15, A14, A11, A12;
verum end; case A17:
i1 > i2
;
ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) )set h1 =
mid (
f,
i2,
i1);
set h2 =
(mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1));
set h3 =
Rev (mid (f,i2,i1));
set h4 =
Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1)));
A18:
L~ (mid (f,i2,i1)) = L~ (Rev (mid (f,i2,i1)))
by SPPOL_2:22;
A19:
for
g being
FinSequence of
(TOP-REAL 2) holds
( not
g is_a_part_of f,
i1,
i2 or
g = Rev (mid (f,i2,i1)) or
g = Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))) )
proof
let g be
FinSequence of
(TOP-REAL 2);
( not g is_a_part_of f,i1,i2 or g = Rev (mid (f,i2,i1)) or g = Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))) )
assume A20:
g is_a_part_of f,
i1,
i2
;
( g = Rev (mid (f,i2,i1)) or g = Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))) )
now per cases
( g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2 )
by A20, Def4;
case
g is_a_part>_of f,
i1,
i2
;
( g = Rev (mid (f,i2,i1)) or g = Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))) )then
Rev g is_a_part<_of f,
i2,
i1
by Th41;
then
Rev g = (mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))
by A17, Th40;
hence
(
g = Rev (mid (f,i2,i1)) or
g = Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))) )
by FINSEQ_6:25;
verum end; case
g is_a_part<_of f,
i1,
i2
;
( g = Rev (mid (f,i2,i1)) or g = Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))) )then
Rev g is_a_part>_of f,
i2,
i1
by Th42;
then
Rev g = mid (
f,
i2,
i1)
by A17, Th37;
hence
(
g = Rev (mid (f,i2,i1)) or
g = Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))) )
by FINSEQ_6:25;
verum end;
hence
(
g = Rev (mid (f,i2,i1)) or
g = Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))) )
;
verum
end; A21:
i1 < len f
by A2, NAT_1:13;
then
mid (
f,
i2,
i1)
is_a_part>_of f,
i2,
i1
by A3, A17, Th43;
then A22:
L~ (Rev (mid (f,i2,i1))) is_S-P_arc_joining f /. i1,
f /. i2
by A17, Th41, Th59;
(L~ (mid (f,i2,i1))) \/ (L~ ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1)))) = L~ f
by A3, A17, A21, Th55;
then A23:
(L~ (Rev (mid (f,i2,i1)))) \/ (L~ (Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))))) = L~ f
by A18, SPPOL_2:22;
(L~ (mid (f,i2,i1))) /\ (L~ ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1)))) = {(f . i2),(f . i1)}
by A3, A17, A21, Th55;
then A24:
(L~ (Rev (mid (f,i2,i1)))) /\ (L~ (Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))))) = {(f . i1),(f . i2)}
by A18, SPPOL_2:22;
Rev (mid (f,i2,i1)) is_a_part<_of f,
i1,
i2
by A3, A17, A21, Th41, Th43;
then A25:
Rev (mid (f,i2,i1)) is_a_part_of f,
i1,
i2
by Def4;
Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))) is_a_part>_of f,
i1,
i2
by A3, A17, A21, Th42, Th46;
then A26:
Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))) is_a_part_of f,
i1,
i2
by Def4;
then
L~ (Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1)))) is_S-P_arc_joining f /. i1,
f /. i2
by A5, Th60;
hence
ex
g1,
g2 being
FinSequence of
(TOP-REAL 2) st
(
g1 is_a_part_of f,
i1,
i2 &
g2 is_a_part_of f,
i1,
i2 &
(L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} &
(L~ g1) \/ (L~ g2) = L~ f &
L~ g1 is_S-P_arc_joining f /. i1,
f /. i2 &
L~ g2 is_S-P_arc_joining f /. i1,
f /. i2 & ( for
g being
FinSequence of
(TOP-REAL 2) holds
( not
g is_a_part_of f,
i1,
i2 or
g = g1 or
g = g2 ) ) )
by A25, A26, A24, A23, A22, A19;
verum end;
hence
ex g1, g2 being FinSequence of (TOP-REAL 2) st
( g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f & L~ g1 is_S-P_arc_joining f /. i1,f /. i2 & L~ g2 is_S-P_arc_joining f /. i1,f /. i2 & ( for g being FinSequence of (TOP-REAL 2) holds
( not g is_a_part_of f,i1,i2 or g = g1 or g = g2 ) ) )
; verum