let f be FinSequence of (TOP-REAL 2); ( 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))}
; 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;
( 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
;
(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 3;
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 3;
(
f /. (i + 1) in LSeg (
(f /. i),
(f /. (i + 1))) &
f /. (i + 1) in LSeg (
(f /. (i + 1)),
(f /. ((i + 1) + 1))) )
by RLTOPSP1:68;
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:31;
A12:
i < len f
by A9, NAT_1:13;
per cases
( i = 1 or i <> 1 )
;
suppose A13:
i <> 1
;
(LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))}now ( ( i + 2 = len f & (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} ) or ( i + 2 <> len f & (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} ) )per cases
( i + 2 = len f or i + 2 <> len f )
;
case A15:
i + 2
<> len f
;
(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:9;
i + 2
< len f
by A5, A15, XXREAL_0:1;
then A17:
((i + 1) + 1) + 1
<= len f
by NAT_1:13;
now not (LSeg (f,i)) /\ (LSeg (f,(i + 1))) <> {(f /. (i + 1))}
(
f /. (i + 1) in LSeg (
f,
(i + 1)) &
f /. (i + 1) in LSeg (
f,
i) )
by A10, A7, RLTOPSP1:68;
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:31;
assume
(LSeg (f,i)) /\ (LSeg (f,(i + 1))) <> {(f /. (i + 1))}
;
contradictionthen
not
(LSeg (f,i)) /\ (LSeg (f,(i + 1))) c= {(f /. (i + 1))}
by A18;
then consider x being
object such that A19:
x in (LSeg (f,i)) /\ (LSeg (f,(i + 1)))
and A20:
not
x in {(f /. (i + 1))}
;
A21:
LSeg (
f,
((i + 1) + 1))
= LSeg (
(f /. ((i + 1) + 1)),
(f /. (((i + 1) + 1) + 1)))
by A8, A17, TOPREAL1:def 3;
A22:
x <> f /. (i + 1)
by A20, TARSKI:def 1;
now ( ( f /. i in LSeg ((f /. (i + 1)),(f /. ((i + 1) + 1))) & contradiction ) or ( f /. ((i + 1) + 1) in LSeg ((f /. i),(f /. (i + 1))) & contradiction ) )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, Th16;
case A23:
f /. i in LSeg (
(f /. (i + 1)),
(f /. ((i + 1) + 1)))
;
contradictionA24:
i -' 1
= i - 1
by A4, XREAL_1:233;
then
(i -' 1) + 1
< i + 1
by NAT_1:13;
then
LSeg (
f,
(i -' 1))
misses LSeg (
f,
(i + 1))
by A1, TOPREAL1:def 7;
then A25:
(LSeg (f,(i -' 1))) /\ (LSeg (f,(i + 1))) = {}
;
LSeg (
f,
(i -' 1))
= LSeg (
(f /. (i -' 1)),
(f /. ((i -' 1) + 1)))
by A12, A16, A24, TOPREAL1:def 3;
then
f /. i in LSeg (
f,
(i -' 1))
by A24, RLTOPSP1:68;
hence
contradiction
by A7, A23, A25, XBOOLE_0:def 4;
verum end; case A26:
f /. ((i + 1) + 1) in LSeg (
(f /. i),
(f /. (i + 1)))
;
contradiction
i + 1
< (i + 1) + 1
by NAT_1:13;
then
LSeg (
f,
i)
misses LSeg (
f,
((i + 1) + 1))
by A1, TOPREAL1:def 7;
then A27:
(LSeg (f,i)) /\ (LSeg (f,((i + 1) + 1))) = {}
;
f /. ((i + 1) + 1) in LSeg (
f,
((i + 1) + 1))
by A21, RLTOPSP1:68;
hence
contradiction
by A10, A26, A27, XBOOLE_0:def 4;
verum end; end; end; hence
contradiction
;
verum end; hence
(LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))}
;
verum end; end; end; hence
(LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))}
;
verum end; end;
end;
hence
f is unfolded
by TOPREAL1:def 6; verum