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