let f be FinSequence of (TOP-REAL 2); :: thesis: for n being Nat holds L~ (f | n) c= L~ f
let n be Nat; :: thesis: L~ (f | n) c= L~ f
now :: thesis: L~ (f | n) c= L~ f
per cases ( n = 0 or n <> 0 ) ;
suppose A1: n = 0 ; :: thesis: L~ (f | n) c= L~ f
thus L~ (f | n) c= L~ f by A1, Th11; :: thesis: verum
end;
suppose A2: n <> 0 ; :: thesis: L~ (f | n) c= L~ f
now :: thesis: L~ (f | n) c= L~ f
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 1;
then len (f /^ n) <> 0 by A3;
then A4: not f /^ n is empty ;
len (f | n) = n by A3, FINSEQ_1:59;
then A5: not f | n is empty by A2;
(f | n) ^ (f /^ n) = f by RFINSEQ:8;
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:58; :: 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