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 A7, A8, NAT_1:13;
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 A10, NAT_1:13;
then i + 1 in dom f by A11, FINSEQ_3:25;
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 A5, FINSEQ_1:22;
then A14: i <= len f by A8, NAT_1:13;
then A15: i = len f by A13, XXREAL_0:1;
i in dom f by A4, A7, A14;
then x1 = y by A2, A9, A15, FINSEQ_1:def 7;
hence x2 in U_FT x1 by A3, A15, FINSEQ_1:42; :: 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: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