let f, g be FinSequence of (TOP-REAL 2); ( f is special & g is special & ( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 ) implies f ^ g is special )
assume that
A1:
f is special
and
A2:
g is special
and
A3:
( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 )
; f ^ g is special
let i be Nat; TOPREAL1:def 5 ( not 1 <= i or not i + 1 <= len (f ^ g) or ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 )
assume that
A4:
1 <= i
and
A5:
i + 1 <= len (f ^ g)
; ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 )
A6:
len (f ^ g) = (len f) + (len g)
by FINSEQ_1:22;
per cases
( i < len f or i = len f or i > len f )
by XXREAL_0:1;
suppose A11:
i > len f
;
( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 )then reconsider j =
i - (len f) as
Element of
NAT by INT_1:5;
(len f) + 1
<= i
by A11, NAT_1:13;
then A12:
1
<= j
by XREAL_1:19;
A13:
(len f) + (j + 1) = i + 1
;
A14:
(i + 1) - (len f) <= len g
by A5, A6, XREAL_1:20;
then
j + 1
in dom g
by A12, SEQ_4:134;
then A15:
(f ^ g) /. (i + 1) = g /. (j + 1)
by A13, FINSEQ_4:69;
A16:
(len f) + j = i
;
j + 1
<= len g
by A14;
then
j in dom g
by A12, SEQ_4:134;
then
(f ^ g) /. i = g /. j
by A16, FINSEQ_4:69;
hence
(
((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or
((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 )
by A2, A12, A14, A15;
verum end;