environ
vocabularies HIDDEN, NUMBERS, PRE_TOPC, EUCLID, FINSEQ_1, SUBSET_1, GOBOARD1, RELAT_1, ARYTM_3, CARD_1, XXREAL_0, TOPREAL1, NAT_1, RLTOPSP1, PARTFUN1, MATRIX_1, FUNCT_1, COMPLEX1, ARYTM_1, ZFMISC_1, TREES_1, INCSP_1, TARSKI, XBOOLE_0, ORDINAL2, MCART_1, ORDINAL4;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, NAT_1, FUNCT_1, PARTFUN1, SEQM_3, FINSEQ_1, PRE_TOPC, MATRIX_0, STRUCT_0, MATRIX_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, XXREAL_0;
definitions TARSKI, TOPREAL1, XBOOLE_0;
theorems TARSKI, NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, ABSVALUE, FINSEQ_3, EUCLID, TOPREAL1, TOPREAL3, GOBOARD1, GOBOARD2, FINSEQ_4, PARTFUN2, INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, PARTFUN1, ORDINAL1, SEQM_3, RLTOPSP1, SEQ_4, MATRIX_0;
schemes NAT_1, FINSEQ_4;
registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, STRUCT_0, EUCLID, INT_1, CARD_1, FINSEQ_1, VALUED_0;
constructors HIDDEN, COMPLEX1, TOPREAL1, GOBOARD1, RELSET_1, DOMAIN_1, MATRIX_1, REAL_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities TOPREAL1, XBOOLE_0;
expansions TARSKI, TOPREAL1, XBOOLE_0;
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;