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