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

hence g /^ k is continuous by A5, A4, A6; :: thesis: verum

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

(len g) -' k >= 0 + 1
by A3, A4, NAT_1:13;
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;(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

hence g /^ k is continuous by A5, A4, A6; :: thesis: verum