let f be FinSequence; :: thesis: for k being Nat holds len (f /^ k) = (len f) -' k
let k be Nat; :: thesis: len (f /^ k) = (len f) -' k

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

suppose A1: k <= len f ; :: thesis: len (f /^ k) = (len f) -' k

then (len f) -' k = (len f) - k by XREAL_1:233;
hence len (f /^ k) = (len f) -' k by A1, Def1; :: thesis: verum

end;

suppose A2: k > len f ; :: thesis: len (f /^ k) = (len f) -' k

then f /^ k = {} by Def1;
then A3: len (f /^ k) = 0 ;
(len f) - k < 0 by A2, XREAL_1:49;
hence len (f /^ k) = (len f) -' k by A3, XREAL_0:def 2; :: thesis: verum

end;

end;