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 that
A1: g is continuous and
A2: k < len g ; :: thesis: g /^ k is continuous
A3: (len g) - k > 0 by A2, XREAL_1:50;
then A4: (len g) - k = (len g) -' k by XREAL_0:def 2;
A5: len (g /^ k) = (len g) - k by A2, RFINSEQ:def 1;
A6: 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 x11
let 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 that
A7: 1 <= i and
A8: i < len (g /^ k) and
A9: x11 = (g /^ k) . i ; :: thesis: (g /^ k) . (i + 1) in U_FT x11
A10: 1 <= 1 + i by NAT_1:11;
i in dom (g /^ k) by A7, A8, FINSEQ_3:25;
then A11: (g /^ k) . i = g . (i + k) by A2, RFINSEQ:def 1;
i <= i + k by NAT_1:11;
then A12: ( (i + 1) + k = (i + k) + 1 & 1 <= i + k ) by A7, XXREAL_0:2;
i + 1 <= (len g) -' k by A5, A4, A8, NAT_1:13;
then i + 1 in dom (g /^ k) by A5, A4, A10, FINSEQ_3:25;
then A13: (g /^ k) . (i + 1) = g . ((i + 1) + k) by A2, RFINSEQ:def 1;
i + k < ((len g) - k) + k by A5, A8, XREAL_1:6;
hence (g /^ k) . (i + 1) in U_FT x11 by A1, A9, A11, A13, A12; :: thesis: verum

end;

(len g) -' k >= 0 + 1 by A3, A4, NAT_1:13;
hence g /^ k is continuous by A5, A4, A6; :: thesis: verum