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 ; :: thesis: verum
end;
suppose A3: k <= len g ; :: thesis: g | k is continuous
hence len (g | k) >= 1 by ; :: 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 ;
then A8: (g | k) . i = g . i by ;
i + 1 <= k by ;
then A9: (g | k) . (i + 1) = g . (i + 1) by FINSEQ_3:112;
i < len g by ;
hence (g | k) . (i + 1) in U_FT x11 by A1, A4, A6, A8, A9; :: thesis: verum
end;
end;