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

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

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

end;

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

then A11: i + 1 > len f by NAT_1:13;
A12: len (f ^ g) = (len f) + (len g) by FINSEQ_1:35;
then A13: i + 1 <= (len f) + (len g) by A5, NAT_1:13;
A14: i < (len f) + (len g) by A5, FINSEQ_1:35;

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

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

A16: x2 = g . ((i + 1) - (len f)) by A11, A12, A13, FINSEQ_1:37
.= g . 1 by A15 ;
A17: len f in dom f by A2, FINSEQ_3:27;
then x1 = f . (len f) by A5, A15, FINSEQ_1:def 7
.= f /. (len f) by A17, PARTFUN1:def 8 ;
hence (f ^ g) . (i + 1) in U_FT x1 by A1, A16; :: thesis: verum

end;

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

then A19: i - (len f) > 0 by XREAL_1:52;
then A20: i -' (len f) = i - (len f) by XREAL_0:def 2;
A21: i >= (len f) + 1 by A18, NAT_1:13;
set j = i -' (len f);
(i -' (len f)) + 1 = (i + 1) - (len f) by A20;
then A22: x2 = g . ((i -' (len f)) + 1) by A11, A12, A13, FINSEQ_1:37;
A23: x1 = g . (i -' (len f)) by A5, A14, A20, A21, FINSEQ_1:36;
A24: i -' (len f) >= 0 + 1 by A19, A20, NAT_1:13;
i - (len f) < len g by A14, XREAL_1:21;
hence (f ^ g) . (i + 1) in U_FT x1 by A1, A20, A22, A23, A24, Def6; :: thesis: verum

end;

end;

end;

end;