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 A1: ( g is continuous & 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:79; :: thesis: verum

end;

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

hence len (g | k) >= 1 by A1, FINSEQ_1:80; :: 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
A3: len (g | k) = k by A2, FINSEQ_1:80;
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 A4: ( 1 <= i & i < len (g | k) & x11 = (g | k) . i ) ; :: thesis: (g | k) . (i + 1) in U_FT x11
then A5: (g | k) . i = g . i by A3, FINSEQ_3:121;
i + 1 <= k by A3, A4, NAT_1:13;
then A6: (g | k) . (i + 1) = g . (i + 1) by FINSEQ_3:121;
i < len g by A2, A3, A4, XXREAL_0:2;
hence (g | k) . (i + 1) in U_FT x11 by A1, A4, A5, A6, Def6; :: thesis: verum

end;

end;