let f be non empty special FinSequence of (TOP-REAL 2); :: thesis: for g being non trivial special FinSequence of (TOP-REAL 2) st f /. (len f) = g /. 1 holds
f ^' g is special
let g be non trivial special FinSequence of (TOP-REAL 2); :: thesis: ( f /. (len f) = g /. 1 implies f ^' g is special )
assume A1: f /. (len f) = g /. 1 ; :: thesis: f ^' g is special
set h = (2,(len g)) -cut g;
A2: f ^' g = f ^ ((2,(len g)) -cut g) by FINSEQ_6:def 5;
A3: 1 + 1 <= len g by NAT_D:60;
then A4: ( (g /. 1) `1 = (g /. (1 + 1)) `1 or (g /. 1) `2 = (g /. (1 + 1)) `2 ) by TOPREAL1:def 5;
len g <= (len g) + 1 by NAT_1:11;
then A5: 2 <= (len g) + 1 by A3, XXREAL_0:2;
((len ((2,(len g)) -cut g)) + 1) + 1 = (len ((2,(len g)) -cut g)) + (1 + 1)
.= (len g) + 1 by A5, Lm1 ;
then 1 <= len ((2,(len g)) -cut g) by A3, XREAL_1:6;
then A6: ((2,(len g)) -cut g) /. 1 = ((2,(len g)) -cut g) . 1 by FINSEQ_4:15
.= g . (1 + 1) by A3, FINSEQ_6:138
.= g /. (1 + 1) by A3, FINSEQ_4:15 ;
(2,(len g)) -cut g is special by Th25;
hence f ^' g is special by A1, A2, A6, A4, GOBOARD2:8; :: thesis: verum