begin
Lm1:
now
let f be
FinSequence of
(TOP-REAL 2);
for k being Element of NAT st len f = k + 1 & k <> 0 & f is unfolded holds
f | k is unfolded let k be
Element of
NAT ;
( len f = k + 1 & k <> 0 & f is unfolded implies f | k is unfolded )A1:
dom (f | k) = Seg (len (f | k))
by FINSEQ_1:def 3;
assume A2:
len f = k + 1
;
( k <> 0 & f is unfolded implies f | k is unfolded )then A3:
len (f | k) = k
by FINSEQ_1:80, NAT_1:11;
assume
k <> 0
;
( f is unfolded implies f | k is unfolded )then A4:
0 + 1
<= k
by NAT_1:13;
assume A5:
f is
unfolded
;
f | k is unfolded A6:
k <= k + 1
by NAT_1:11;
then A7:
k in dom f
by A2, A4, FINSEQ_3:27;
thus
f | k is
unfolded
verum
proof
let n be
Nat;
TOPREAL1:def 8 ( not 1 <= n or not n + 2 <= len (f | k) or (LSeg (f | k),n) /\ (LSeg (f | k),(n + 1)) = {((f | k) /. (n + 1))} )
set f1 =
f | k;
assume that A8:
1
<= n
and A9:
n + 2
<= len (f | k)
;
(LSeg (f | k),n) /\ (LSeg (f | k),(n + 1)) = {((f | k) /. (n + 1))}
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
A10:
n + 1
in dom (f | k)
by A8, A9, SEQ_4:152;
n in dom (f | k)
by A8, A9, SEQ_4:152;
then A11:
LSeg (f | k),
n = LSeg f,
n
by A10, TOPREAL3:24;
len (f | k) <= len f
by A2, A6, FINSEQ_1:80;
then A12:
n + 2
<= len f
by A9, XXREAL_0:2;
A13:
(n + 1) + 1
= n + (1 + 1)
;
n + 2
in dom (f | k)
by A8, A9, SEQ_4:152;
then A14:
LSeg (f | k),
(n + 1) = LSeg f,
(n + 1)
by A10, A13, TOPREAL3:24;
(f | k) /. (n + 1) = f /. (n + 1)
by A7, A3, A1, A10, FINSEQ_4:86;
hence
(LSeg (f | k),n) /\ (LSeg (f | k),(n + 1)) = {((f | k) /. (n + 1))}
by A5, A8, A11, A14, A12, TOPREAL1:def 8;
verum
end;
end;
theorem Th1:
theorem