let f be circular unfolded s.c.c. FinSequence of (TOP-REAL 2); :: thesis: ( len f > 4 implies (LSeg (f,1)) /\ (L~ (f /^ 1)) = {(f /. 1),(f /. 2)} )
assume A1: len f > 4 ; :: thesis: (LSeg (f,1)) /\ (L~ (f /^ 1)) = {(f /. 1),(f /. 2)}
A2: 1 + 2 <= len f by A1, XXREAL_0:2;
set h2 = f /^ 1;
A3: 1 <= len f by A1, XXREAL_0:2;
then A4: len (f /^ 1) = (len f) - 1 by RFINSEQ:def 1;
then A5: (len (f /^ 1)) + 1 = len f ;
len f > 3 + 1 by A1;
then A6: len (f /^ 1) > 2 + 1 by A5, XREAL_1:6;
then A7: 1 + 1 <= len (f /^ 1) by XXREAL_0:2;
set SFY = { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ;
set Reszta = union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ;
A8: ((len (f /^ 1)) -' 1) + 1 <= len (f /^ 1) by A6, XREAL_1:235, XXREAL_0:2;
A9: 1 < len f by A1, XXREAL_0:2;
for Z being set holds
( Z in {{}} iff ex X, Y being set st
( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y ) )
proof
let Z be set ; :: thesis: ( Z in {{}} iff ex X, Y being set st
( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y ) )
thus ( Z in {{}} implies ex X, Y being set st
( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y ) ) :: thesis: ( ex X, Y being set st
( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y ) implies Z in {{}} )
proof
assume A10: Z in {{}} ; :: thesis: ex X, Y being set st
( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y )
take X = LSeg (f,1); :: thesis: ex Y being set st
( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y )
take Y = LSeg (f,(2 + 1)); :: thesis: ( X in {(LSeg (f,1))} & Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y )
thus X in {(LSeg (f,1))} by TARSKI:def 1; :: thesis: ( Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } & Z = X /\ Y )
Y = LSeg ((f /^ 1),2) by A3, SPPOL_2:4;
hence Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } by A6; :: thesis: Z = X /\ Y
A11: 1 + 1 < 3 ;
3 + 1 < len f by A1;
then X misses Y by A11, GOBOARD5:def 4;
then X /\ Y = {} by XBOOLE_0:def 7;
hence Z = X /\ Y by A10, TARSKI:def 1; :: thesis: verum
end;
given X, Y being set such that A12: X in {(LSeg (f,1))} and
A13: Y in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } and
A14: Z = X /\ Y ; :: thesis: Z in {{}}
A15: X = LSeg (f,1) by A12, TARSKI:def 1;
consider i being Nat such that
A16: Y = LSeg ((f /^ 1),i) and
A17: 1 < i and
A18: i + 1 < len (f /^ 1) by A13;
A19: 1 + 1 < i + 1 by A17, XREAL_1:6;
A20: (i + 1) + 1 < len f by A5, A18, XREAL_1:6;
LSeg ((f /^ 1),i) = LSeg (f,(i + 1)) by A9, A17, SPPOL_2:4;
then X misses Y by A15, A16, A20, A19, GOBOARD5:def 4;
then Z = {} by A14, XBOOLE_0:def 7;
hence Z in {{}} by TARSKI:def 1; :: thesis: verum
end;
then INTERSECTION ({(LSeg (f,1))}, { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ) = {{}} by SETFAM_1:def 5;
then A21: (LSeg (f,1)) /\ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ) = union {{}} by SETFAM_1:25
.= {} by ZFMISC_1:25 ;
A22: L~ (f /^ 1) c= ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } )
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in L~ (f /^ 1) or u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ) )
assume u in L~ (f /^ 1) ; :: thesis: u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } )
then consider e being set such that
A23: u in e and
A24: e in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f /^ 1) ) } by TARSKI:def 4;
consider i being Nat such that
A25: e = LSeg ((f /^ 1),i) and
A26: 1 <= i and
A27: i + 1 <= len (f /^ 1) by A24;
per cases ( i = 1 or i + 1 = len (f /^ 1) or ( 1 < i & i + 1 < len (f /^ 1) ) ) by A26, A27, XXREAL_0:1;
suppose i = 1 ; :: thesis: u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } )
then u in (LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1))) by A23, A25, XBOOLE_0:def 3;
hence u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose i + 1 = len (f /^ 1) ; :: thesis: u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } )
then i = (len (f /^ 1)) -' 1 by NAT_D:34;
then u in (LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1))) by A23, A25, XBOOLE_0:def 3;
hence u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose ( 1 < i & i + 1 < len (f /^ 1) ) ; :: thesis: u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } )
then e in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } by A25;
then u in union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } by A23, TARSKI:def 4;
hence u in ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
A28: union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } c= L~ (f /^ 1)
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } or u in L~ (f /^ 1) )
assume u in union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ; :: thesis: u in L~ (f /^ 1)
then consider e being set such that
A29: u in e and
A30: e in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } by TARSKI:def 4;
ex i being Nat st
( e = LSeg ((f /^ 1),i) & 1 < i & i + 1 < len (f /^ 1) ) by A30;
then e in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f /^ 1) ) } ;
hence u in L~ (f /^ 1) by A29, TARSKI:def 4; :: thesis: verum
end;
1 + ((len (f /^ 1)) -' 1) = len (f /^ 1) by A6, XREAL_1:235, XXREAL_0:2
.= (len f) -' 1 by A1, A4, XREAL_1:233, XXREAL_0:2 ;
then A31: (LSeg (f,1)) /\ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1))) = (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) by A3, A7, NAT_D:55, SPPOL_2:4
.= {(f /. 1)} by A1, REVROT_1:30 ;
1 + 1 <= len (f /^ 1) by A6, NAT_1:13;
then LSeg ((f /^ 1),1) in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f /^ 1) ) } ;
then A32: LSeg ((f /^ 1),1) c= L~ (f /^ 1) by ZFMISC_1:74;
A33: (LSeg (f,1)) /\ (LSeg ((f /^ 1),1)) = (LSeg (f,1)) /\ (LSeg (f,(1 + 1))) by A3, SPPOL_2:4
.= {(f /. (1 + 1))} by A2, TOPREAL1:def 6 ;
1 <= (len (f /^ 1)) -' 1 by A7, NAT_D:55;
then LSeg ((f /^ 1),((len (f /^ 1)) -' 1)) in { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f /^ 1) ) } by A8;
then LSeg ((f /^ 1),((len (f /^ 1)) -' 1)) c= L~ (f /^ 1) by ZFMISC_1:74;
then (LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1))) c= L~ (f /^ 1) by A32, XBOOLE_1:8;
then ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ) c= L~ (f /^ 1) by A28, XBOOLE_1:8;
then L~ (f /^ 1) = ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1)))) \/ (union { (LSeg ((f /^ 1),i)) where i is Nat : ( 1 < i & i + 1 < len (f /^ 1) ) } ) by A22, XBOOLE_0:def 10;
hence (LSeg (f,1)) /\ (L~ (f /^ 1)) = ((LSeg (f,1)) /\ ((LSeg ((f /^ 1),1)) \/ (LSeg ((f /^ 1),((len (f /^ 1)) -' 1))))) \/ {} by A21, XBOOLE_1:23
.= {(f /. 1)} \/ {(f /. 2)} by A33, A31, XBOOLE_1:23
.= {(f /. 1),(f /. 2)} by ENUMSET1:1 ;
:: thesis: verum