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, FINSEQ_6:159;
A3: 1 < len g by Th2;
then A4: (f ^' g) /. (((len f) + 0) + 1) = g /. ((0 + 1) + 1) by FINSEQ_6:160;
A5: 1 + 1 <= len g by A3, NAT_1:13;
((len f) + 0) + 1 < (len f) + (len g) by A3, XREAL_1:6;
then ((len f) + 0) + 1 < (len (f ^' g)) + 1 by FINSEQ_6:139;
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 3
.= LSeg (g,1) by A2, A4, A5, TOPREAL1:def 3 ;
:: thesis: verum