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
A2: f ^' g = f ^ (2,(len g) -cut g) by GRAPH_2:def 2;
set h = 2,(len g) -cut g;
A3: 1 + 1 <= len g by REALSET1:13;
len g <= (len g) + 1 by NAT_1:11;
then A4: 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 A4, Lm1 ;
then 1 <= len (2,(len g) -cut g) by A3, XREAL_1:8;
then A5: (2,(len g) -cut g) /. 1 = (2,(len g) -cut g) . 1 by FINSEQ_4:24
.= g . (1 + 1) by A3, GRAPH_2:12
.= g /. (1 + 1) by A3, FINSEQ_4:24 ;
A6: 2,(len g) -cut g is special by Th25;
( (g /. 1) `1 = (g /. (1 + 1)) `1 or (g /. 1) `2 = (g /. (1 + 1)) `2 ) by A3, TOPREAL1:def 7;
hence f ^' g is special by A1, A2, A5, A6, GOBOARD2:13; :: thesis: verum