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

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