let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis: ( f1 is special & f2 is special & ( (f1 /. (len f1)) `1 = (f2 /. 1) `1 or (f1 /. (len f1)) `2 = (f2 /. 1) `2 ) implies f1 ^ f2 is special )
assume that
A1: f1 is special and
A2: f2 is special and
A3: ( (f1 /. (len f1)) `1 = (f2 /. 1) `1 or (f1 /. (len f1)) `2 = (f2 /. 1) `2 ) ; :: thesis: f1 ^ f2 is special
set f = f1 ^ f2;
let n be Nat; :: according to TOPREAL1:def 7 :: thesis: ( not 1 <= n or not n + 1 <= len (f1 ^ f2) or ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 )
assume A4: ( 1 <= n & n + 1 <= len (f1 ^ f2) ) ; :: thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 )
reconsider n = n as Element of NAT by ORDINAL1:def 13;
set p = (f1 ^ f2) /. n;
set q = (f1 ^ f2) /. (n + 1);
A5: ( dom f1 = Seg (len f1) & dom f2 = Seg (len f2) & len (f1 ^ f2) = (len f1) + (len f2) & (n + 1) - (len f1) = (n - (len f1)) + 1 ) by FINSEQ_1:35, FINSEQ_1:def 3;

per cases ( n + 1 <= len f1 or len f1 < n + 1 ) ;

suppose A6: n + 1 <= len f1 ; :: thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 )

then ( n in dom f1 & n + 1 in dom f1 ) by A4, Th3;
then ( f1 /. n = (f1 ^ f2) /. n & f1 /. (n + 1) = (f1 ^ f2) /. (n + 1) ) by FINSEQ_4:83;
hence ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) by A1, A4, A6, TOPREAL1:def 7; :: thesis: verum

end;

suppose len f1 < n + 1 ; :: thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 )

then A7: len f1 <= n by NAT_1:13;
then reconsider n1 = n - (len f1) as Element of NAT by INT_1:18;

now

per cases ( n = len f1 or n <> len f1 ) ;

suppose A8: n = len f1 ; :: thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 )

then n in dom f1 by A4, FINSEQ_3:27;
then A9: (f1 ^ f2) /. n = f1 /. n by FINSEQ_4:83;
len f2 >= 1 by A4, A5, A8, XREAL_1:8;
hence ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) by A3, A8, A9, Th5; :: thesis: verum

end;

suppose n <> len f1 ; :: thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 )

then A10: ( len f1 < n & n <= n + 1 ) by A7, NAT_1:11, XXREAL_0:1;
then ( (len f1) + 1 <= n & len f1 < n + 1 & n + 1 <= len (f1 ^ f2) ) by A4, NAT_1:13;
then A11: ( 1 <= n1 & n <= len (f1 ^ f2) ) by A10, XREAL_1:21, XXREAL_0:2;
A12: n = n1 + (len f1) ;
A13: n + 1 = (n1 + 1) + (len f1) ;
then A14: n1 + 1 <= len f2 by A4, A5, XREAL_1:8;
n1 + 1 >= n1 by NAT_1:11;
then n1 <= len f2 by A14, XXREAL_0:2;
then A15: f2 /. n1 = (f1 ^ f2) /. n by A11, A12, Th5;
f2 /. (n1 + 1) = (f1 ^ f2) /. (n + 1) by A13, A14, Th5, NAT_1:11;
hence ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) by A2, A11, A14, A15, TOPREAL1:def 7; :: thesis: verum

end;

end;

end;

hence ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) ; :: thesis: verum

end;

end;