let f be FinSequence of (TOP-REAL 2); :: thesis: for n being Element of NAT holds L~ (f | n) c= L~ f
let n be Element of NAT ; :: thesis: L~ (f | n) c= L~ f

now

per cases ( n = 0 or n <> 0 ) ;

suppose A1: n = 0 ; :: thesis: L~ (f | n) c= L~ f

f | 0 is empty ;
hence L~ (f | n) c= L~ f by A1, Th11, XBOOLE_1:2; :: thesis: verum

end;

suppose A2: n <> 0 ; :: thesis: L~ (f | n) c= L~ f

now

per cases ( n < len f or n >= len f ) ;

suppose A3: n < len f ; :: thesis: L~ (f | n) c= L~ f

then len (f /^ n) = (len f) - n by RFINSEQ:def 2;
then len (f /^ n) <> 0 by A3;
then A4: not f /^ n is empty ;
len (f | n) = n by A3, FINSEQ_1:80;
then A5: not f | n is empty by A2;
(f | n) ^ (f /^ n) = f by RFINSEQ:21;
then L~ f = ((L~ (f | n)) \/ (LSeg ((f | n) /. (len (f | n))),((f /^ n) /. 1))) \/ (L~ (f /^ n)) by A5, A4, Th23
.= (L~ (f | n)) \/ ((LSeg ((f | n) /. (len (f | n))),((f /^ n) /. 1)) \/ (L~ (f /^ n))) by XBOOLE_1:4 ;
hence L~ (f | n) c= L~ f by XBOOLE_1:7; :: thesis: verum

end;

suppose n >= len f ; :: thesis: L~ (f | n) c= L~ f

hence L~ (f | n) c= L~ f by FINSEQ_1:79; :: thesis: verum

end;

end;

end;

hence L~ (f | n) c= L~ f ; :: thesis: verum

end;

end;

end;

hence L~ (f | n) c= L~ f ; :: thesis: verum