let f be XFinSequence; :: thesis: for n being Nat st n < len f holds
len (f /^ n) = (len f) - n
let n be Nat; :: thesis: ( n < len f implies len (f /^ n) = (len f) - n )
assume n < len f ; :: thesis: len (f /^ n) = (len f) - n
then (len f) - n >= 0 by XREAL_1:50;
then (len f) -' n = (len f) - n by XREAL_0:def 2;
hence len (f /^ n) = (len f) - n by Def2; :: thesis: verum