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

.= (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

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

len (f ^ <*x*>) =
(len f) + (len <*x*>)
by FINSEQ_1:22
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 ;

end;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 x1end;

hence
g . (i + 1) in U_FT x1
; :: thesis: verumper cases
( i < len f or i >= len f )
;

end;

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;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

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;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

.= (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