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

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

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

hence g | k is continuous by A1, FINSEQ_1:58; :: thesis: verum

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;

end;