let FT be non empty RelStr ; :: thesis: for f being FinSequence of FT
for x, y being Element of FT st f is continuous & y = f . (len f) & x in U_FT y holds
f ^ <*x*> is continuous

let f be FinSequence of FT; :: thesis: for x, y being Element of FT st f is continuous & y = f . (len f) & x in U_FT y holds
f ^ <*x*> is continuous

let x, y be Element of FT; :: thesis: ( f is continuous & y = f . (len f) & x in U_FT y implies f ^ <*x*> is continuous )
assume that
A1: f is continuous and
A2: y = f . (len f) and
A3: x in U_FT y ; :: thesis: f ^ <*x*> is continuous
reconsider g = f ^ <*x*> as FinSequence of FT ;
A4: dom f = Seg (len f) by FINSEQ_1:def 3;
A5: len <*x*> = 1 by FINSEQ_1:39;
A6: for i being Nat
for x1 being Element of FT st 1 <= i & i < len g & x1 = g . i holds
g . (i + 1) in U_FT x1
proof
let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len g & x1 = g . i holds
g . (i + 1) in U_FT x1

let x1 be Element of FT; :: thesis: ( 1 <= i & i < len g & x1 = g . i implies g . (i + 1) in U_FT x1 )
assume that
A7: 1 <= i and
A8: i < len g and
A9: x1 = g . i ; :: thesis: g . (i + 1) in U_FT x1
( i + 1 <= len g & 1 < i + 1 ) by ;
then i + 1 in dom g by FINSEQ_3:25;
then g . (i + 1) = g /. (i + 1) by PARTFUN1:def 6;
then reconsider x2 = g . (i + 1) as Element of FT ;
now :: thesis: x2 in U_FT x1
per cases ( i < len f or i >= len f ) ;
suppose A10: i < len f ; :: thesis: x2 in U_FT x1
A11: 1 <= i + 1 by NAT_1:11;
i + 1 <= len f by ;
then i + 1 in dom f by ;
then A12: g . (i + 1) = f . (i + 1) by FINSEQ_1:def 7;
i in dom f by A4, A7, A10;
then g . i = f . i by FINSEQ_1:def 7;
hence x2 in U_FT x1 by A1, A7, A9, A10, A12; :: thesis: verum
end;
suppose A13: i >= len f ; :: thesis: x2 in U_FT x1
len g = (len f) + 1 by ;
then A14: i <= len f by ;
then A15: i = len f by ;
i in dom f by A4, A7, A14;
then x1 = y by ;
hence x2 in U_FT x1 by ; :: thesis: verum
end;
end;
end;
hence g . (i + 1) in U_FT x1 ; :: thesis: verum
end;
len (f ^ <*x*>) = (len f) + () by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39 ;
then len (f ^ <*x*>) >= 1 by NAT_1:11;
hence f ^ <*x*> is continuous by A6; :: thesis: verum