Lm1:
now for f being FinSequence of (TOP-REAL 2)
for k being Nat st len f = k + 1 & k <> 0 & f is unfolded holds
f | k is unfolded
let f be
FinSequence of
(TOP-REAL 2);
for k being Nat st len f = k + 1 & k <> 0 & f is unfolded holds
f | k is unfolded let k be
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:59, 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:25;
thus
f | k is
unfolded
verum
proof
let n be
Nat;
TOPREAL1:def 6 ( 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 12;
A10:
n + 1
in dom (f | k)
by A8, A9, SEQ_4:135;
n in dom (f | k)
by A8, A9, SEQ_4:135;
then A11:
LSeg (
(f | k),
n)
= LSeg (
f,
n)
by A10, TOPREAL3:17;
len (f | k) <= len f
by A2, A6, FINSEQ_1:59;
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:135;
then A14:
LSeg (
(f | k),
(n + 1))
= LSeg (
f,
(n + 1))
by A10, A13, TOPREAL3:17;
(f | k) /. (n + 1) = f /. (n + 1)
by A7, A3, A1, A10, FINSEQ_4:71;
hence
(LSeg ((f | k),n)) /\ (LSeg ((f | k),(n + 1))) = {((f | k) /. (n + 1))}
by A5, A8, A11, A14, A12;
verum
end;
end;