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
let n be Nat; :: according to TOPREAL1:def 5 :: 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 )
set f = f1 ^ f2;
assume that
A4: 1 <= n and
A5: 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 12;
set p = (f1 ^ f2) /. n;
set q = (f1 ^ f2) /. (n + 1);
A6: len (f1 ^ f2) = (len f1) + (len f2) by FINSEQ_1:22;
per cases ( n + 1 <= len f1 or len f1 < n + 1 ) ;
suppose A7: 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 + 1 in dom f1 by A4, SEQ_4:134;
then A8: f1 /. (n + 1) = (f1 ^ f2) /. (n + 1) by FINSEQ_4:68;
n in dom f1 by A4, A7, SEQ_4:134;
then f1 /. n = (f1 ^ f2) /. n by FINSEQ_4:68;
hence ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) by A1, A4, A7, A8; :: 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 A9: len f1 <= n by NAT_1:13;
then reconsider n1 = n - (len f1) as Element of NAT by INT_1:5;
now :: thesis: ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 )
per cases ( n = len f1 or n <> len f1 ) ;
suppose A10: 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:25;
then A11: (f1 ^ f2) /. n = f1 /. n by FINSEQ_4:68;
len f2 >= 1 by A5, A6, A10, XREAL_1:6;
hence ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) by A3, A10, A11, SEQ_4:136; :: 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 len f1 < n by A9, XXREAL_0:1;
then (len f1) + 1 <= n by NAT_1:13;
then A12: 1 <= n1 by XREAL_1:19;
A13: n + 1 = (n1 + 1) + (len f1) ;
then A14: n1 + 1 <= len f2 by A5, A6, XREAL_1:6;
then A15: f2 /. (n1 + 1) = (f1 ^ f2) /. (n + 1) by A13, NAT_1:11, SEQ_4:136;
n1 + 1 >= n1 by NAT_1:11;
then ( n = n1 + (len f1) & n1 <= len f2 ) by A14, XXREAL_0:2;
then f2 /. n1 = (f1 ^ f2) /. n by A12, SEQ_4:136;
hence ( ((f1 ^ f2) /. n) `1 = ((f1 ^ f2) /. (n + 1)) `1 or ((f1 ^ f2) /. n) `2 = ((f1 ^ f2) /. (n + 1)) `2 ) by A2, A12, A14, A15; :: 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;