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 ;

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

end;

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

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;

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

end;

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

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