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 ;
then A4: (len g) - k = (len g) -' k by XREAL_0:def 2;
A5: len (g /^ k) = (len g) - k by ;
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 ;
then A11: (g /^ k) . i = g . (i + k) by ;
i <= i + k by NAT_1:11;
then A12: ( (i + 1) + k = (i + k) + 1 & 1 <= i + k ) by ;
i + 1 <= (len g) -' k by ;
then i + 1 in dom (g /^ k) by ;
then A13: (g /^ k) . (i + 1) = g . ((i + 1) + k) by ;
i + k < ((len g) - k) + k by ;
hence (g /^ k) . (i + 1) in U_FT x11 by A1, A9, A11, A13, A12; :: thesis: verum
end;
(len g) -' k >= 0 + 1 by ;
hence g /^ k is continuous by A5, A4, A6; :: thesis: verum