let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is nodic & PairF f is Simple & f . 1 <> f . (len f) implies f is unfolded )
assume that
A1: f is nodic and
A2: ( PairF f is Simple & f . 1 <> f . (len f) ) ; :: thesis: f is unfolded

per cases ( 2 < len f or len f <= 2 ) ;

suppose A3: 2 < len f ; :: thesis: f is unfolded

then A4: 2 + 1 <= len f by NAT_1:13;
then A5: 2 + 1 in dom f by FINSEQ_3:27;
A6: f . 2 = f /. 2 by A3, FINSEQ_4:24;
then A7: f . 2 in LSeg (f,2) by A4, TOPREAL1:27;
1 + 1 <= len f by A3;
then f . 2 in LSeg (f,1) by A6, TOPREAL1:27;
then (LSeg (f,1)) /\ (LSeg (f,2)) <> {} by A7, XBOOLE_0:def 4;
then A8: LSeg (f,1) meets LSeg (f,2) by XBOOLE_0:def 7;
A9: len f < (len f) + 1 by NAT_1:13;
then A10: (len f) - 1 < len f by XREAL_1:21;
A11: 2 in dom f by A3, FINSEQ_3:27;
A12: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by A3, TOPREAL1:def 5;
A13: f is one-to-one by A2, Th22;
A14: 1 < len f by A3, XXREAL_0:2;
then A15: 1 in dom f by FINSEQ_3:27;
A16: f . 1 = f /. 1 by A14, FINSEQ_4:24;
A17: (len f) -' 2 = (len f) - 2 by A3, XREAL_1:235;
A18: LSeg (f,2) = LSeg ((f /. 2),(f /. (2 + 1))) by A4, TOPREAL1:def 5;

now

assume A19: LSeg (f,1) = LSeg (f,2) ; :: thesis: contradiction

now

per cases ( ( f /. 1 = f /. 2 & f /. (1 + 1) = f /. (2 + 1) ) or ( f /. 1 = f /. (2 + 1) & f /. (1 + 1) = f /. 2 ) ) by A12, A18, A19, SPPOL_1:25;

case A20: ( f /. 1 = f /. 2 & f /. (1 + 1) = f /. (2 + 1) ) ; :: thesis: contradiction

( f . 1 = f /. 1 & f . 2 = f /. 2 ) by A3, A14, FINSEQ_4:24;
hence contradiction by A13, A15, A11, A20, FUNCT_1:def 8; :: thesis: verum

end;

case A21: ( f /. 1 = f /. (2 + 1) & f /. (1 + 1) = f /. 2 ) ; :: thesis: contradiction

f . (2 + 1) = f /. (2 + 1) by A4, FINSEQ_4:24;
hence contradiction by A13, A15, A16, A5, A21, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then ( ( (LSeg (f,1)) /\ (LSeg (f,2)) = {(f . 1)} & ( f . 1 = f . 2 or f . 1 = f . (2 + 1) ) ) or ( (LSeg (f,1)) /\ (LSeg (f,2)) = {(f . (1 + 1))} & ( f . (1 + 1) = f . 2 or f . (1 + 1) = f . (2 + 1) ) ) ) by A1, A8, Def4;
then A22: (LSeg (f,1)) /\ (LSeg (f,(1 + 1))) c= {(f /. (1 + 1))} by A3, A13, A15, A5, FINSEQ_4:24, FUNCT_1:def 8;
A23: (len f) - 1 = (len f) -' 1 by A3, XREAL_1:235, XXREAL_0:2;
then A24: ((len f) -' 1) + 1 in dom f by A14, FINSEQ_3:27;
A25: (1 + 1) - 1 <= (len f) - 1 by A3, XREAL_1:11;
then A26: f . ((len f) -' 1) = f /. ((len f) -' 1) by A23, A10, FINSEQ_4:24;
A27: (2 + 1) - 2 <= (len f) - 2 by A4, XREAL_1:11;
then A28: LSeg (f,((len f) -' 2)) = LSeg ((f /. ((len f) -' 2)),(f /. (((len f) -' 2) + 1))) by A17, A10, TOPREAL1:def 5;
A29: ((len f) - 1) - 1 < (len f) - 1 by A10, XREAL_1:11;
then (len f) - 2 < len f by A10, XXREAL_0:2;
then A30: f . ((len f) -' 2) = f /. ((len f) -' 2) by A27, A17, FINSEQ_4:24;
A31: (len f) -' 2 < len f by A17, A10, A29, XXREAL_0:2;
then A32: (len f) -' 2 in dom f by A27, A17, FINSEQ_3:27;
A33: LSeg (f,((len f) -' 1)) = LSeg ((f /. ((len f) -' 1)),(f /. (((len f) -' 1) + 1))) by A25, A23, TOPREAL1:def 5;
A34: f . ((len f) -' 2) = f /. ((len f) -' 2) by A27, A17, A31, FINSEQ_4:24;

A35: now

assume A36: LSeg (f,((len f) -' 2)) = LSeg (f,((len f) -' 1)) ; :: thesis: contradiction
A37: (len f) -' 2 in dom f by A27, A17, A31, FINSEQ_3:27;
A38: (len f) -' 1 in dom f by A25, A23, A10, FINSEQ_3:27;

now

per cases ( ( f /. ((len f) -' 2) = f /. ((len f) -' 1) & f /. (((len f) -' 2) + 1) = f /. (((len f) -' 1) + 1) ) or ( f /. ((len f) -' 2) = f /. (((len f) -' 1) + 1) & f /. (((len f) -' 2) + 1) = f /. ((len f) -' 1) ) ) by A28, A33, A36, SPPOL_1:25;

case A39: ( f /. ((len f) -' 2) = f /. ((len f) -' 1) & f /. (((len f) -' 2) + 1) = f /. (((len f) -' 1) + 1) ) ; :: thesis: contradiction

f . ((len f) -' 1) = f /. ((len f) -' 1) by A25, A23, A10, FINSEQ_4:24;
hence contradiction by A13, A23, A17, A9, A34, A37, A38, A39, FUNCT_1:def 8; :: thesis: verum

end;

case A40: ( f /. ((len f) -' 2) = f /. (((len f) -' 1) + 1) & f /. (((len f) -' 2) + 1) = f /. ((len f) -' 1) ) ; :: thesis: contradiction

((len f) -' 1) + 1 in Seg (len f) by A14, A23, FINSEQ_1:3;
then A41: ((len f) -' 1) + 1 in dom f by FINSEQ_1:def 3;
f . (((len f) -' 1) + 1) = f /. (((len f) -' 1) + 1) by A14, A23, FINSEQ_4:24;
hence contradiction by A13, A23, A17, A10, A29, A30, A37, A40, A41, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

((len f) -' 1) + 1 = len f by A23;
then A42: f . ((len f) -' 1) in LSeg (f,((len f) -' 1)) by A25, A26, TOPREAL1:27;
((len f) -' 2) + 1 = (len f) - ((1 + 1) - 1) by A17;
then f . ((len f) -' 1) in LSeg (f,((len f) -' 2)) by A27, A23, A10, A26, TOPREAL1:27;
then (LSeg (f,((len f) -' 2))) /\ (LSeg (f,((len f) -' 1))) <> {} by A42, XBOOLE_0:def 4;
then LSeg (f,((len f) -' 2)) meets LSeg (f,((len f) -' 1)) by XBOOLE_0:def 7;
then ( ( (LSeg (f,((len f) -' 2))) /\ (LSeg (f,((len f) -' 1))) = {(f . ((len f) -' 2))} & ( f . ((len f) -' 2) = f . ((len f) -' 1) or f . ((len f) -' 2) = f . (((len f) -' 1) + 1) ) ) or ( (LSeg (f,((len f) -' 2))) /\ (LSeg (f,((len f) -' 1))) = {(f . (((len f) -' 2) + 1))} & ( f . (((len f) -' 2) + 1) = f . ((len f) -' 1) or f . (((len f) -' 2) + 1) = f . (((len f) -' 1) + 1) ) ) ) by A1, A35, Def4;
then (LSeg (f,((len f) -' 2))) /\ (LSeg (f,((len f) -' 1))) c= {(f /. ((len f) -' 1))} by A13, A25, A23, A17, A10, A29, A32, A24, FINSEQ_4:24, FUNCT_1:def 8;
hence f is unfolded by A1, A2, A22, Th19, Th21; :: thesis: verum

end;

suppose A43: len f <= 2 ; :: 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
A44: 1 <= i and
A45: i + 2 <= len f ; :: thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))}
i + 2 <= 2 by A43, A45, XXREAL_0:2;
then i <= 2 - 2 by XREAL_1:21;
hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A44, XXREAL_0:2; :: thesis: verum

end;

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

end;

end;