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:25;
A6: f . 2 = f /. 2 by A3, FINSEQ_4:15;
then A7: f . 2 in LSeg (f,2) by A4, TOPREAL1:21;
1 + 1 <= len f by A3;
then f . 2 in LSeg (f,1) by A6, TOPREAL1:21;
then (LSeg (f,1)) /\ (LSeg (f,2)) <> {} by A7, XBOOLE_0:def 4;
then A8: LSeg (f,1) meets LSeg (f,2) ;
A9: len f < (len f) + 1 by NAT_1:13;
then A10: (len f) - 1 < len f by XREAL_1:19;
A11: 2 in dom f by A3, FINSEQ_3:25;
A12: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by A3, TOPREAL1:def 3;
A13: f is one-to-one by A2, Th18;
A14: 1 < len f by A3, XXREAL_0:2;
then A15: 1 in dom f by FINSEQ_3:25;
A16: f . 1 = f /. 1 by A14, FINSEQ_4:15;
A17: (len f) -' 2 = (len f) - 2 by A3, XREAL_1:233;
A18: LSeg (f,2) = LSeg ((f /. 2),(f /. (2 + 1))) by A4, TOPREAL1:def 3;
now :: thesis: not LSeg (f,1) = LSeg (f,2)
assume A19: LSeg (f,1) = LSeg (f,2) ; :: thesis: contradiction
now :: thesis: ( ( f /. 1 = f /. 2 & f /. (1 + 1) = f /. (2 + 1) & contradiction ) or ( f /. 1 = f /. (2 + 1) & f /. (1 + 1) = f /. 2 & contradiction ) )
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:8;
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:15;
hence contradiction by A13, A15, A11, A20; :: 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:15;
hence contradiction by A13, A15, A16, A5, A21; :: 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;
then A22: (LSeg (f,1)) /\ (LSeg (f,(1 + 1))) c= {(f /. (1 + 1))} by A3, A13, A15, A5, FINSEQ_4:15;
A23: (len f) - 1 = (len f) -' 1 by A3, XREAL_1:233, XXREAL_0:2;
then A24: ((len f) -' 1) + 1 in dom f by A14, FINSEQ_3:25;
A25: (1 + 1) - 1 <= (len f) - 1 by A3, XREAL_1:9;
then A26: f . ((len f) -' 1) = f /. ((len f) -' 1) by A23, A10, FINSEQ_4:15;
A27: (2 + 1) - 2 <= (len f) - 2 by A4, XREAL_1:9;
then A28: LSeg (f,((len f) -' 2)) = LSeg ((f /. ((len f) -' 2)),(f /. (((len f) -' 2) + 1))) by A17, A10, TOPREAL1:def 3;
A29: ((len f) - 1) - 1 < (len f) - 1 by A10, XREAL_1:9;
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:15;
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:25;
A33: LSeg (f,((len f) -' 1)) = LSeg ((f /. ((len f) -' 1)),(f /. (((len f) -' 1) + 1))) by A25, A23, TOPREAL1:def 3;
A34: f . ((len f) -' 2) = f /. ((len f) -' 2) by A27, A17, A31, FINSEQ_4:15;
A35: now :: thesis: not LSeg (f,((len f) -' 2)) = LSeg (f,((len f) -' 1))
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:25;
A38: (len f) -' 1 in dom f by A25, A23, A10, FINSEQ_3:25;
now :: thesis: ( ( f /. ((len f) -' 2) = f /. ((len f) -' 1) & f /. (((len f) -' 2) + 1) = f /. (((len f) -' 1) + 1) & contradiction ) or ( f /. ((len f) -' 2) = f /. (((len f) -' 1) + 1) & f /. (((len f) -' 2) + 1) = f /. ((len f) -' 1) & contradiction ) )
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:8;
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:15;
hence contradiction by A13, A23, A17, A9, A34, A37, A38, A39; :: 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:1;
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:15;
hence contradiction by A13, A23, A17, A10, A29, A30, A37, A40, A41; :: 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:21;
((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:21;
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)) ;
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;
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:15;
hence f is unfolded by A1, A2, A22, Th15, Th17; :: 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:19;
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 6; :: thesis: verum
end;
end;