let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is s.n.c. & (LSeg f,1) /\ (LSeg f,(1 + 1)) c= {(f /. (1 + 1))} & (LSeg f,((len f) -' 2)) /\ (LSeg f,((len f) -' 1)) c= {(f /. ((len f) -' 1))} implies f is unfolded )
assume that
A1: f is s.n.c. and
A2: (LSeg f,1) /\ (LSeg f,(1 + 1)) c= {(f /. (1 + 1))} and
A3: (LSeg f,((len f) -' 2)) /\ (LSeg f,((len f) -' 1)) c= {(f /. ((len f) -' 1))} ; :: thesis: f is unfolded
for i being Nat st 1 <= i & i + 2 <= len f holds
(LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))}

proof

let i be Nat; :: thesis: ( 1 <= i & i + 2 <= len f implies (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} )
assume that
A4: 1 <= i and
A5: i + 2 <= len f ; :: thesis: (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))}
A6: 1 < i + 1 by A4, NAT_1:13;
then A7: LSeg f,(i + 1) = LSeg (f /. (i + 1)),(f /. ((i + 1) + 1)) by A5, TOPREAL1:def 5;
A8: 1 < (i + 1) + 1 by A6, NAT_1:13;
(i + 1) + 1 = i + 2 ;
then A9: i + 1 < len f by A5, NAT_1:13;
then A10: LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A4, TOPREAL1:def 5;
( f /. (i + 1) in LSeg (f /. i),(f /. (i + 1)) & f /. (i + 1) in LSeg (f /. (i + 1)),(f /. ((i + 1) + 1)) ) by RLTOPSP1:69;
then f /. (i + 1) in (LSeg f,i) /\ (LSeg f,(i + 1)) by A10, A7, XBOOLE_0:def 4;
then A11: {(f /. (i + 1))} c= (LSeg f,i) /\ (LSeg f,(i + 1)) by ZFMISC_1:37;
A12: i < len f by A9, NAT_1:13;

per cases ( i = 1 or i <> 1 ) ;

suppose i = 1 ; :: thesis: (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))}

hence (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} by A2, A11, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A13: i <> 1 ; :: thesis: (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))}

now

per cases ( i + 2 = len f or i + 2 <> len f ) ;

case A14: i + 2 = len f ; :: thesis: (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))}

then ( (len f) - 2 = (len f) -' 2 & (len f) - 1 = (len f) -' 1 ) by A4, A6, NAT_D:39;
hence (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} by A3, A11, A14, XBOOLE_0:def 10; :: thesis: verum

end;

case A15: i + 2 <> len f ; :: thesis: (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))}

1 < i by A4, A13, XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then A16: (1 + 1) - 1 <= i - 1 by XREAL_1:11;
i + 2 < len f by A5, A15, XXREAL_0:1;
then A17: ((i + 1) + 1) + 1 <= len f by NAT_1:13;

now

( f /. (i + 1) in LSeg f,(i + 1) & f /. (i + 1) in LSeg f,i ) by A10, A7, RLTOPSP1:69;
then f /. (i + 1) in (LSeg f,i) /\ (LSeg f,(i + 1)) by XBOOLE_0:def 4;
then A18: {(f /. (i + 1))} c= (LSeg f,i) /\ (LSeg f,(i + 1)) by ZFMISC_1:37;
assume (LSeg f,i) /\ (LSeg f,(i + 1)) <> {(f /. (i + 1))} ; :: thesis: contradiction
then not (LSeg f,i) /\ (LSeg f,(i + 1)) c= {(f /. (i + 1))} by A18, XBOOLE_0:def 10;
then consider x being set such that
A19: x in (LSeg f,i) /\ (LSeg f,(i + 1)) and
A20: not x in {(f /. (i + 1))} by TARSKI:def 3;
A21: LSeg f,((i + 1) + 1) = LSeg (f /. ((i + 1) + 1)),(f /. (((i + 1) + 1) + 1)) by A8, A17, TOPREAL1:def 5;
A22: x <> f /. (i + 1) by A20, TARSKI:def 1;

now

per cases ( f /. i in LSeg (f /. (i + 1)),(f /. ((i + 1) + 1)) or f /. ((i + 1) + 1) in LSeg (f /. i),(f /. (i + 1)) ) by A10, A7, A19, A22, Th20;

case A23: f /. i in LSeg (f /. (i + 1)),(f /. ((i + 1) + 1)) ; :: thesis: contradiction

A24: i -' 1 = i - 1 by A4, XREAL_1:235;
then (i -' 1) + 1 < i + 1 by NAT_1:13;
then LSeg f,(i -' 1) misses LSeg f,(i + 1) by A1, TOPREAL1:def 9;
then A25: (LSeg f,(i -' 1)) /\ (LSeg f,(i + 1)) = {} by XBOOLE_0:def 7;
LSeg f,(i -' 1) = LSeg (f /. (i -' 1)),(f /. ((i -' 1) + 1)) by A12, A16, A24, TOPREAL1:def 5;
then f /. i in LSeg f,(i -' 1) by A24, RLTOPSP1:69;
hence contradiction by A7, A23, A25, XBOOLE_0:def 4; :: thesis: verum

end;

case A26: f /. ((i + 1) + 1) in LSeg (f /. i),(f /. (i + 1)) ; :: thesis: contradiction

i + 1 < (i + 1) + 1 by NAT_1:13;
then LSeg f,i misses LSeg f,((i + 1) + 1) by A1, TOPREAL1:def 9;
then A27: (LSeg f,i) /\ (LSeg f,((i + 1) + 1)) = {} by XBOOLE_0:def 7;
f /. ((i + 1) + 1) in LSeg f,((i + 1) + 1) by A21, RLTOPSP1:69;
hence contradiction by A10, A26, A27, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} ; :: thesis: verum

end;

end;

end;

hence (LSeg f,i) /\ (LSeg f,(i + 1)) = {(f /. (i + 1))} ; :: thesis: verum

end;

end;

end;

hence f is unfolded by TOPREAL1:def 8; :: thesis: verum