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

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