let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( 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 ) ; :: thesis: f ^ g is special
let i be Nat; :: according to TOPREAL1:def 7 :: thesis: ( 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) ; :: thesis: ( ((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:35;

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

suppose i < len f ; :: thesis: ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 )

then A7: i + 1 <= len f by NAT_1:13;
then i in dom f by A4, GOBOARD2:3;
then A8: (f ^ g) /. i = f /. i by FINSEQ_4:83;
i + 1 in dom f by A4, A7, GOBOARD2:3;
then (f ^ g) /. (i + 1) = f /. (i + 1) by FINSEQ_4:83;
hence ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 ) by A1, A4, A7, A8, TOPREAL1:def 7; :: thesis: verum

end;

suppose A9: i = len f ; :: thesis: ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 )

then i in dom f by A4, FINSEQ_3:27;
then A10: (f ^ g) /. i = f /. i by FINSEQ_4:83;
1 <= len g by A5, A6, A9, XREAL_1:8;
then 1 in dom g by FINSEQ_3:27;
hence ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 ) by A3, A9, A10, FINSEQ_4:84; :: thesis: verum

end;

suppose A11: i > len f ; :: thesis: ( ((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:18;
A12: (len f) + j = i ;
A13: (len f) + (j + 1) = i + 1 ;
(len f) + 1 <= i by A11, NAT_1:13;
then A14: 1 <= j by XREAL_1:21;
A15: (i + 1) - (len f) <= len g by A5, A6, XREAL_1:22;
then j + 1 <= len g ;
then j in dom g by A14, GOBOARD2:3;
then A16: (f ^ g) /. i = g /. j by A12, FINSEQ_4:84;
j + 1 in dom g by A14, A15, GOBOARD2:3;
then (f ^ g) /. (i + 1) = g /. (j + 1) by A13, FINSEQ_4:84;
hence ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 ) by A2, A14, A15, A16, TOPREAL1:def 7; :: thesis: verum

end;

end;