let n be Nat; :: thesis: for f being FinSequence of REAL st not (f | n) /^ 1 is empty holds
len ((f | n) /^ 1) <= (len f) - 1
let f be FinSequence of REAL ; :: thesis: ( not (f | n) /^ 1 is empty implies len ((f | n) /^ 1) <= (len f) - 1 )
assume not (f | n) /^ 1 is empty ; :: thesis: len ((f | n) /^ 1) <= (len f) - 1
then not f | n is empty ;
then A2: 1 in dom (f | n) by FINSEQ_5:6;
f | n = ((f | n) | 1) ^ ((f | n) /^ 1) by RFINSEQ:8;
then len (f | n) = (len ((f | n) | 1)) + (len ((f | n) /^ 1)) by FINSEQ_1:22;
then A3: (len ((f | n) /^ 1)) + 1 = len (f | n) by A2, Th10;
(len (f | n)) - 1 <= (len f) - 1 by XREAL_1:9, FINSEQ_5:16;
hence len ((f | n) /^ 1) <= (len f) - 1 by A3; :: thesis: verum