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 A1: ( f is nodic & PairF f is Simple & f . 1 <> f . (len f) ) ; :: thesis: f is unfolded

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

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

then A3: 2 + 1 <= len f by NAT_1:13;
A4: 1 + 1 <= len f by A2;
A5: LSeg f,1 = LSeg (f /. 1),(f /. (1 + 1)) by A2, TOPREAL1:def 5;
A6: LSeg f,2 = LSeg (f /. 2),(f /. (2 + 1)) by A3, TOPREAL1:def 5;
A7: f is one-to-one by A1, Th22;
A8: 1 < len f by A2, XXREAL_0:2;
then A9: 1 in dom f by FINSEQ_3:27;
A10: 2 in dom f by A2, FINSEQ_3:27;
A11: f . 1 = f /. 1 by A8, FINSEQ_4:24;
A12: 2 + 1 in dom f by A3, FINSEQ_3:27;
A13: f . 2 = f /. 2 by A2, FINSEQ_4:24;
then A14: f . 2 in LSeg f,1 by A4, TOPREAL1:27;

A15: now

assume A16: 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 A5, A6, A16, SPPOL_1:25;

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

A18: f . 1 = f /. 1 by A8, FINSEQ_4:24;
f . 2 = f /. 2 by A2, FINSEQ_4:24;
hence contradiction by A7, A9, A10, A17, A18, FUNCT_1:def 8; :: thesis: verum

end;

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

f . (2 + 1) = f /. (2 + 1) by A3, FINSEQ_4:24;
hence contradiction by A7, A9, A11, A12, A19, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

f . 2 in LSeg f,2 by A3, A13, TOPREAL1:27;
then (LSeg f,1) /\ (LSeg f,2) <> {} by A14, XBOOLE_0:def 4;
then LSeg f,1 meets LSeg f,2 by XBOOLE_0:def 7;
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, A15, Def4;
then A20: (LSeg f,1) /\ (LSeg f,(1 + 1)) c= {(f /. (1 + 1))} by A2, A7, A9, A12, FINSEQ_4:24, FUNCT_1:def 8;
A21: (1 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:11;
A22: (2 + 1) - 2 <= (len f) - 2 by A3, XREAL_1:11;
A23: (len f) - 1 = (len f) -' 1 by A2, XREAL_1:235, XXREAL_0:2;
then A24: ((len f) -' 1) + 1 = len f ;
A25: (len f) -' 2 = (len f) - 2 by A2, XREAL_1:235;
then A26: ((len f) -' 2) + 1 = (len f) - ((1 + 1) - 1) ;
A27: len f < (len f) + 1 by NAT_1:13;
then A28: (len f) - 1 < len f by XREAL_1:21;
then A29: ((len f) - 1) - 1 < (len f) - 1 by XREAL_1:11;
then A30: (len f) - 2 < len f by A28, XXREAL_0:2;
A31: (len f) -' 2 < len f by A25, A28, A29, XXREAL_0:2;
A32: LSeg f,((len f) -' 2) = LSeg (f /. ((len f) -' 2)),(f /. (((len f) -' 2) + 1)) by A22, A25, A28, TOPREAL1:def 5;
A33: LSeg f,((len f) -' 1) = LSeg (f /. ((len f) -' 1)),(f /. (((len f) -' 1) + 1)) by A21, A23, TOPREAL1:def 5;
A34: f . ((len f) -' 2) = f /. ((len f) -' 2) by A22, A25, A31, FINSEQ_4:24;
A35: f . ((len f) -' 2) = f /. ((len f) -' 2) by A22, A25, A30, FINSEQ_4:24;

A36: now

assume A37: LSeg f,((len f) -' 2) = LSeg f,((len f) -' 1) ; :: thesis: contradiction
A38: (len f) -' 2 in dom f by A22, A25, A31, FINSEQ_3:27;
A39: (len f) -' 1 in dom f by A21, A23, A28, 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 A32, A33, A37, SPPOL_1:25;

case A40: ( 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 A21, A23, A28, FINSEQ_4:24;
hence contradiction by A7, A23, A25, A27, A34, A38, A39, A40, FUNCT_1:def 8; :: thesis: verum

end;

case A41: ( 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 A8, A23, FINSEQ_1:3;
then A42: ((len f) -' 1) + 1 in dom f by FINSEQ_1:def 3;
f . (((len f) -' 1) + 1) = f /. (((len f) -' 1) + 1) by A8, A23, FINSEQ_4:24;
hence contradiction by A7, A23, A25, A28, A29, A35, A38, A41, A42, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

A43: f . ((len f) -' 1) = f /. ((len f) -' 1) by A21, A23, A28, FINSEQ_4:24;
then A44: f . ((len f) -' 1) in LSeg f,((len f) -' 2) by A22, A23, A26, A28, TOPREAL1:27;
f . ((len f) -' 1) in LSeg f,((len f) -' 1) by A21, A24, A43, TOPREAL1:27;
then (LSeg f,((len f) -' 2)) /\ (LSeg f,((len f) -' 1)) <> {} by A44, XBOOLE_0:def 4;
then LSeg f,((len f) -' 2) meets LSeg f,((len f) -' 1) by XBOOLE_0:def 7;
then A45: ( ( (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, A36, Def4;
A46: (len f) -' 2 in dom f by A22, A25, A31, FINSEQ_3:27;
((len f) -' 1) + 1 in dom f by A8, A23, FINSEQ_3:27;
then (LSeg f,((len f) -' 2)) /\ (LSeg f,((len f) -' 1)) c= {(f /. ((len f) -' 1))} by A7, A21, A23, A25, A28, A29, A45, A46, FINSEQ_4:24, FUNCT_1:def 8;
hence f is unfolded by A1, A20, Th19, Th21; :: thesis: verum

end;

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

end;

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

end;

end;