let FT be non empty RelStr ; :: thesis: for g being FinSequence of FT
for k being Element of NAT st g is continuous & k < len g holds
g /^ k is continuous
let g be FinSequence of FT; :: thesis: for k being Element of NAT st g is continuous & k < len g holds
g /^ k is continuous
let k be Element of NAT ; :: thesis: ( g is continuous & k < len g implies g /^ k is continuous )
assume A1:
( g is continuous & k < len g )
; :: thesis: g /^ k is continuous
then A2:
len (g /^ k) = (len g) - k
by RFINSEQ:def 2;
A3:
(len g) - k > 0
by A1, XREAL_1:52;
then A4:
(len g) - k = (len g) -' k
by XREAL_0:def 2;
then A5:
(len g) -' k >= 0 + 1
by A3, NAT_1:13;
for i being Nat
for x11 being Element of FT st 1 <= i & i < len (g /^ k) & x11 = (g /^ k) . i holds
(g /^ k) . (i + 1) in U_FT x11
proof
let i be
Nat;
:: thesis: for x11 being Element of FT st 1 <= i & i < len (g /^ k) & x11 = (g /^ k) . i holds
(g /^ k) . (i + 1) in U_FT x11let x11 be
Element of
FT;
:: thesis: ( 1 <= i & i < len (g /^ k) & x11 = (g /^ k) . i implies (g /^ k) . (i + 1) in U_FT x11 )
assume A6:
( 1
<= i &
i < len (g /^ k) &
x11 = (g /^ k) . i )
;
:: thesis: (g /^ k) . (i + 1) in U_FT x11
then
i in dom (g /^ k)
by FINSEQ_3:27;
then A7:
(g /^ k) . i = g . (i + k)
by A1, RFINSEQ:def 2;
A8:
i + 1
<= (len g) -' k
by A2, A4, A6, NAT_1:13;
1
<= 1
+ i
by NAT_1:11;
then
i + 1
in dom (g /^ k)
by A2, A4, A8, FINSEQ_3:27;
then A9:
(g /^ k) . (i + 1) = g . ((i + 1) + k)
by A1, RFINSEQ:def 2;
A10:
(i + 1) + k = (i + k) + 1
;
i <= i + k
by NAT_1:11;
then A11:
1
<= i + k
by A6, XXREAL_0:2;
i + k < ((len g) - k) + k
by A2, A6, XREAL_1:8;
hence
(g /^ k) . (i + 1) in U_FT x11
by A1, A6, A7, A9, A10, A11, Def6;
:: thesis: verum
end;
hence
g /^ k is continuous
by A2, A4, A5, Def6; :: thesis: verum