let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for g being non trivial FinSequence of (TOP-REAL 2) st f /. (len f) = g /. 1 holds
LSeg (f ^' g),(len f) = LSeg g,1
A1: 1 <= len f by NAT_1:14;
let g be non trivial FinSequence of (TOP-REAL 2); :: thesis: ( f /. (len f) = g /. 1 implies LSeg (f ^' g),(len f) = LSeg g,1 )
assume f /. (len f) = g /. 1 ; :: thesis: LSeg (f ^' g),(len f) = LSeg g,1
then A2: (f ^' g) /. ((len f) + 0 ) = g /. (0 + 1) by A1, GRAPH_2:61;
A3: 1 < len g by Th2;
then A4: (f ^' g) /. (((len f) + 0 ) + 1) = g /. ((0 + 1) + 1) by GRAPH_2:62;
A5: 1 + 1 <= len g by A3, NAT_1:13;
((len f) + 0 ) + 1 < (len f) + (len g) by A3, XREAL_1:8;
then ((len f) + 0 ) + 1 < (len (f ^' g)) + 1 by GRAPH_2:13;
then ((len f) + 0 ) + 1 <= len (f ^' g) by NAT_1:13;
hence LSeg (f ^' g),(len f) = LSeg ((f ^' g) /. ((len f) + 0 )),((f ^' g) /. (((len f) + 0 ) + 1)) by A1, TOPREAL1:def 5
.= LSeg g,1 by A2, A4, A5, TOPREAL1:def 5 ;
:: thesis: verum