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 A1: ( f is continuous & y = f . (len f) & x in U_FT y ) ; :: thesis: f ^ <*x*> is continuous
reconsider g = f ^ <*x*> as FinSequence of FT ;
A2: dom f = Seg (len f) by FINSEQ_1:def 3;
A3: len <*x*> = 1 by FINSEQ_1:56;
A4: 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 A5: ( 1 <= i & i < len g & x1 = g . i ) ; :: thesis: g . (i + 1) in U_FT x1
then A6: i + 1 <= len g by NAT_1:13;
1 < i + 1 by A5, NAT_1:13;
then i + 1 in dom g by A6, FINSEQ_3:27;
then g . (i + 1) = g /. (i + 1) by PARTFUN1:def 8;
then reconsider x2 = g . (i + 1) as Element of FT ;

now

per cases ( i < len f or i >= len f ) ;

suppose A7: i < len f ; :: thesis: x2 in U_FT x1

then A8: i + 1 <= len f by NAT_1:13;
1 <= i + 1 by NAT_1:11;
then i + 1 in dom f by A8, FINSEQ_3:27;
then A9: g . (i + 1) = f . (i + 1) by FINSEQ_1:def 7;
i in dom f by A2, A5, A7, FINSEQ_1:3;
then g . i = f . i by FINSEQ_1:def 7;
hence x2 in U_FT x1 by A1, A5, A7, A9, Def6; :: thesis: verum

end;

suppose A10: i >= len f ; :: thesis: x2 in U_FT x1

len g = (len f) + 1 by A3, FINSEQ_1:35;
then A11: i <= len f by A5, NAT_1:13;
then A12: i = len f by A10, XXREAL_0:1;
i in dom f by A2, A5, A11, FINSEQ_1:3;
then x1 = y by A1, A5, A12, FINSEQ_1:def 7;
hence x2 in U_FT x1 by A1, A12, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

hence g . (i + 1) in U_FT x1 ; :: thesis: verum

end;

len (f ^ <*x*>) = (len f) + (len <*x*>) by FINSEQ_1:35
.= (len f) + 1 by FINSEQ_1:56 ;
then len (f ^ <*x*>) >= 1 by NAT_1:11;
hence f ^ <*x*> is continuous by A4, Def6; :: thesis: verum