let f be non constant standard special_circular_sequence; :: thesis: 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 ; :: thesis: ( 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 A1:
( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & i1 <> i2 )
; :: thesis: 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 A2:
i1 <= i2
;
:: thesis: 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 ) ) )then A3:
i1 < i2
by A1, XXREAL_0:1;
A4:
i2 < len f
by A1, NAT_1:13;
set h1 =
mid f,
i1,
i2;
set h2 =
(mid f,i1,1) ^ (mid f,((len f) -' 1),i2);
A5:
mid f,
i1,
i2 is_a_part>_of f,
i1,
i2
by A1, A2, A4, Th43;
(mid f,i1,1) ^ (mid f,((len f) -' 1),i2) is_a_part<_of f,
i1,
i2
by A1, A3, A4, Th46;
then A6:
(
mid f,
i1,
i2 is_a_part_of f,
i1,
i2 &
(mid f,i1,1) ^ (mid f,((len f) -' 1),i2) is_a_part_of f,
i1,
i2 )
by A5, Def4;
A7:
(
(L~ (mid f,i1,i2)) /\ (L~ ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2))) = {(f . i1),(f . i2)} &
(L~ (mid f,i1,i2)) \/ (L~ ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2))) = L~ f )
by A1, A3, A4, Th55;
A8:
L~ (mid f,i1,i2) is_S-P_arc_joining f /. i1,
f /. i2
by A3, A5, Th56;
A9:
L~ ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) is_S-P_arc_joining f /. i1,
f /. i2
by A1, A6, Th60;
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);
:: thesis: ( 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 A10:
g is_a_part_of f,
i1,
i2
;
:: thesis: ( 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) )
;
:: thesis: 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 ) ) )
by A6, A7, A8, A9;
:: thesis: verum end; case A11:
i1 > i2
;
:: thesis: 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 ) ) )A12:
i1 < len f
by A1, NAT_1:13;
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));
A13:
(
(L~ (mid f,i2,i1)) /\ (L~ ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1))) = {(f . i2),(f . i1)} &
(L~ (mid f,i2,i1)) \/ (L~ ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1))) = L~ f )
by A1, A11, A12, Th55;
A14:
L~ (mid f,i2,i1) = L~ (Rev (mid f,i2,i1))
by SPPOL_2:22;
A15:
mid f,
i2,
i1 is_a_part>_of f,
i2,
i1
by A1, A11, A12, Th43;
A16:
Rev (mid f,i2,i1) is_a_part<_of f,
i1,
i2
by A1, A11, A12, Th41, Th43;
Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)) is_a_part>_of f,
i1,
i2
by A1, A11, A12, Th42, Th46;
then A17:
(
Rev (mid f,i2,i1) is_a_part_of f,
i1,
i2 &
Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)) is_a_part_of f,
i1,
i2 )
by A16, Def4;
A18:
(
(L~ (Rev (mid f,i2,i1))) /\ (L~ (Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)))) = {(f . i1),(f . i2)} &
(L~ (Rev (mid f,i2,i1))) \/ (L~ (Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)))) = L~ f )
by A13, A14, SPPOL_2:22;
A19:
L~ (Rev (mid f,i2,i1)) is_S-P_arc_joining f /. i1,
f /. i2
by A11, A15, Th41, Th59;
A20:
L~ (Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1))) is_S-P_arc_joining f /. i1,
f /. i2
by A1, A17, Th60;
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);
:: thesis: ( 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 A21:
g is_a_part_of f,
i1,
i2
;
:: thesis: ( 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 A21, Def4;
case
g is_a_part>_of f,
i1,
i2
;
:: thesis: ( 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 A11, Th40;
hence
(
g = Rev (mid f,i2,i1) or
g = Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)) )
by FINSEQ_6:29;
:: thesis: verum end; case
g is_a_part<_of f,
i1,
i2
;
:: thesis: ( 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 A11, Th37;
hence
(
g = Rev (mid f,i2,i1) or
g = Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)) )
by FINSEQ_6:29;
:: thesis: verum end;
hence
(
g = Rev (mid f,i2,i1) or
g = Rev ((mid f,i2,1) ^ (mid f,((len f) -' 1),i1)) )
;
:: thesis: 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 ) ) )
by A17, A18, A19, A20;
:: thesis: 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 ) ) )
; :: thesis: verum