let f be V26() standard special_circular_sequence; :: thesis: for i1, i2 being 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 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 that
A1: 1 <= i1 and
A2: i1 + 1 <= len f and
A3: 1 <= i2 and
A4: i2 + 1 <= len f and
A5: 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 :: thesis: ( ( 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 ) ) ) ) or ( 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 ) ) ) ) )
per cases ( i1 <= i2 or i1 > i2 ) ;
case A6: 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 ) ) )
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, Th31;
then A9: mid (f,i1,i2) is_a_part_of f,i1,i2 ;
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, Th44;
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); :: 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 A13: 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)) )
now :: thesis: ( ( 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)) ) ) or ( 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)) ) ) )
per cases ( g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2 ) by A13;
case 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)) ) by A6, Th25; :: thesis: verum
end;
case 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)) ) by A10, Th28; :: thesis: verum
end;
end;
end;
hence ( g = mid (f,i1,i2) or g = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) ) ; :: thesis: 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, Th43;
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, Th43;
(mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part<_of f,i1,i2 by A1, A10, A7, Th34;
then A16: (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part_of f,i1,i2 ;
then L~ ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) is_S-P_arc_joining f /. i1,f /. i2 by A5, Th48;
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; :: thesis: verum
end;
case A17: 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 ) ) )
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); :: 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 A20: 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 :: thesis: ( ( 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))) ) ) or ( 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))) ) ) )
per cases ( g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2 ) by A20;
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 Th29;
then Rev g = (mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1)) by A17, Th28;
hence ( g = Rev (mid (f,i2,i1)) or g = Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))) ) ; :: 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 Th30;
then Rev g = mid (f,i2,i1) by A17, Th25;
hence ( g = Rev (mid (f,i2,i1)) or g = Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))) ) ; :: thesis: verum
end;
end;
end;
hence ( g = Rev (mid (f,i2,i1)) or g = Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))) ) ; :: thesis: 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, Th31;
then A22: L~ (Rev (mid (f,i2,i1))) is_S-P_arc_joining f /. i1,f /. i2 by A17, Th29, Th47;
(L~ (mid (f,i2,i1))) \/ (L~ ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1)))) = L~ f by A3, A17, A21, Th43;
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, Th43;
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, Th29, Th31;
then A25: 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 A3, A17, A21, Th30, Th34;
then A26: Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1))) is_a_part_of f,i1,i2 ;
then L~ (Rev ((mid (f,i2,1)) ^ (mid (f,((len f) -' 1),i1)))) is_S-P_arc_joining f /. i1,f /. i2 by A5, Th48;
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; :: thesis: verum
end;
end;
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