let FT be non empty RelStr ; :: thesis: for f, g being FinSequence of FT st f is continuous & g is continuous & g . 1 in U_FT (f /. (len f)) holds
f ^ g is continuous
let f, g be FinSequence of FT; :: thesis: ( f is continuous & g is continuous & g . 1 in U_FT (f /. (len f)) implies f ^ g is continuous )
assume that
A1: f is continuous and
A2: g is continuous and
A3: g . 1 in U_FT (f /. (len f)) ; :: thesis: f ^ g is continuous
A4: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
len g >= 1 by A2;
then len (f ^ g) >= 0 + 1 by A4, XREAL_1:7;
hence len (f ^ g) >= 1 ; :: according to FINTOPO6:def 6 :: thesis: for i being Nat
for x1 being Element of FT st 1 <= i & i < len (f ^ g) & x1 = (f ^ g) . i holds
(f ^ g) . (i + 1) in U_FT x1
let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len (f ^ g) & x1 = (f ^ g) . i holds
(f ^ g) . (i + 1) in U_FT x1
let x1 be Element of FT; :: thesis: ( 1 <= i & i < len (f ^ g) & x1 = (f ^ g) . i implies (f ^ g) . (i + 1) in U_FT x1 )
set g2 = f ^ g;
A5: dom f = Seg (len f) by FINSEQ_1:def 3;
A6: len f >= 1 by A1;
assume that
A7: 1 <= i and
A8: i < len (f ^ g) and
A9: x1 = (f ^ g) . i ; :: thesis: (f ^ g) . (i + 1) in U_FT x1
( i + 1 <= len (f ^ g) & 1 < i + 1 ) by A7, A8, NAT_1:13;
then i + 1 in dom (f ^ g) by FINSEQ_3:25;
then (f ^ g) . (i + 1) = (f ^ g) /. (i + 1) by PARTFUN1:def 6;
then reconsider x2 = (f ^ g) . (i + 1) as Element of FT ;

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

suppose A10: i < len f ; :: thesis: (f ^ g) . (i + 1) 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: (f ^ g) . (i + 1) = f . (i + 1) by FINSEQ_1:def 7;
i in dom f by A5, A7, A10;
then (f ^ g) . i = f . i by FINSEQ_1:def 7;
hence (f ^ g) . (i + 1) in U_FT x1 by A1, A7, A9, A10, A12; :: thesis: verum

end;

suppose A13: i >= len f ; :: thesis: (f ^ g) . (i + 1) in U_FT x1

then A14: i + 1 > len f by NAT_1:13;
A15: i < (len f) + (len g) by A8, FINSEQ_1:22;
A16: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
then A17: i + 1 <= (len f) + (len g) by A8, NAT_1:13;

per cases ( i = len f or i > len f ) by A13, XXREAL_0:1;

suppose A18: i = len f ; :: thesis: (f ^ g) . (i + 1) in U_FT x1

A19: len f in dom f by A6, FINSEQ_3:25;
then A20: x1 = f . (len f) by A9, A18, FINSEQ_1:def 7
.= f /. (len f) by A19, PARTFUN1:def 6 ;
x2 = g . ((i + 1) - (len f)) by A14, A16, A17, FINSEQ_1:24
.= g . 1 by A18 ;
hence (f ^ g) . (i + 1) in U_FT x1 by A3, A20; :: thesis: verum

end;

suppose A21: i > len f ; :: thesis: (f ^ g) . (i + 1) in U_FT x1

set j = i -' (len f);
A22: i - (len f) > 0 by A21, XREAL_1:50;
then A23: i -' (len f) = i - (len f) by XREAL_0:def 2;
then (i -' (len f)) + 1 = (i + 1) - (len f) ;
then A24: x2 = g . ((i -' (len f)) + 1) by A14, A16, A17, FINSEQ_1:24;
A25: i - (len f) < len g by A15, XREAL_1:19;
i >= (len f) + 1 by A21, NAT_1:13;
then A26: x1 = g . (i -' (len f)) by A9, A15, A23, FINSEQ_1:23;
i -' (len f) >= 0 + 1 by A22, A23, NAT_1:13;
hence (f ^ g) . (i + 1) in U_FT x1 by A2, A23, A24, A26, A25; :: thesis: verum

end;

end;

end;

end;