let n be Nat; :: thesis: for f being FinSequence of REAL st not (f | n) /^ 1 is empty holds
len ((f | n) /^ 1) < n
let f be FinSequence of REAL ; :: thesis: ( not (f | n) /^ 1 is empty implies len ((f | n) /^ 1) < n )
assume not (f | n) /^ 1 is empty ; :: thesis: len ((f | n) /^ 1) < n
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) <= n by FINSEQ_5:17;
hence len ((f | n) /^ 1) < n by A3, NAT_1:13; :: thesis: verum