let FT be non empty RelStr ; :: thesis: for g being FinSequence of FT

for k being Nat st g is continuous & 1 <= k holds

g | k is continuous

let g be FinSequence of FT; :: thesis: for k being Nat st g is continuous & 1 <= k holds

g | k is continuous

let k be Nat; :: thesis: ( g is continuous & 1 <= k implies g | k is continuous )

assume that

A1: g is continuous and

A2: 1 <= k ; :: thesis: g | k is continuous

for k being Nat st g is continuous & 1 <= k holds

g | k is continuous

let g be FinSequence of FT; :: thesis: for k being Nat st g is continuous & 1 <= k holds

g | k is continuous

let k be Nat; :: thesis: ( g is continuous & 1 <= k implies g | k is continuous )

assume that

A1: g is continuous and

A2: 1 <= k ; :: thesis: g | k is continuous

per cases
( len g <= k or k <= len g )
;

end;

suppose A3:
k <= len g
; :: thesis: g | k is continuous

hence
len (g | k) >= 1
by A2, FINSEQ_1:59; :: according to FINTOPO6:def 6 :: thesis: for i being Nat

for x1 being Element of FT st 1 <= i & i < len (g | k) & x1 = (g | k) . i holds

(g | k) . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len (g | k) & x1 = (g | k) . i holds

(g | k) . (i + 1) in U_FT x1

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

A4: 1 <= i and

A5: i < len (g | k) and

A6: x11 = (g | k) . i ; :: thesis: (g | k) . (i + 1) in U_FT x11

A7: len (g | k) = k by A3, FINSEQ_1:59;

then A8: (g | k) . i = g . i by A5, FINSEQ_3:112;

i + 1 <= k by A7, A5, NAT_1:13;

then A9: (g | k) . (i + 1) = g . (i + 1) by FINSEQ_3:112;

i < len g by A3, A7, A5, XXREAL_0:2;

hence (g | k) . (i + 1) in U_FT x11 by A1, A4, A6, A8, A9; :: thesis: verum

end;for x1 being Element of FT st 1 <= i & i < len (g | k) & x1 = (g | k) . i holds

(g | k) . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len (g | k) & x1 = (g | k) . i holds

(g | k) . (i + 1) in U_FT x1

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

A4: 1 <= i and

A5: i < len (g | k) and

A6: x11 = (g | k) . i ; :: thesis: (g | k) . (i + 1) in U_FT x11

A7: len (g | k) = k by A3, FINSEQ_1:59;

then A8: (g | k) . i = g . i by A5, FINSEQ_3:112;

i + 1 <= k by A7, A5, NAT_1:13;

then A9: (g | k) . (i + 1) = g . (i + 1) by FINSEQ_3:112;

i < len g by A3, A7, A5, XXREAL_0:2;

hence (g | k) . (i + 1) in U_FT x11 by A1, A4, A6, A8, A9; :: thesis: verum