let f be non trivial FinSequence of (TOP-REAL 2); :: thesis: LSeg f,1 = L~ (f | 2)
A1: 1 + 1 <= len f by REALSET1:13;
then A2: f | 2 = <*(f /. 1),(f /. 2)*> by JORDAN8:1;
thus LSeg f,1 = LSeg (f /. 1),(f /. (1 + 1)) by A1, TOPREAL1:def 5
.= L~ (f | 2) by A2, SPPOL_2:21 ; :: thesis: verum