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 ;
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 ;
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 ;
then i + 1 in dom f by ;
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 ;
A16: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
then A17: i + 1 <= (len f) + (len g) by ;
per cases ( i = len f or i > len f ) by ;
suppose A18: i = len f ; :: thesis: (f ^ g) . (i + 1) in U_FT x1
A19: len f in dom f by ;
then A20: x1 = f . (len f) by
.= f /. (len f) by ;
x2 = g . ((i + 1) - (len f)) by
.= g . 1 by A18 ;
hence (f ^ g) . (i + 1) in U_FT x1 by ; :: 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 ;
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 ;
A25: i - (len f) < len g by ;
i >= (len f) + 1 by ;
then A26: x1 = g . (i -' (len f)) by ;
i -' (len f) >= 0 + 1 by ;
hence (f ^ g) . (i + 1) in U_FT x1 by A2, A23, A24, A26, A25; :: thesis: verum
end;
end;
end;
end;