per cases ( n > 0 or n = 0 ) ;

suppose A1: n > 0 ; :: thesis: (f | n) /^ n is empty

( len (f | n) = n or not n in dom f ) by Th10;
then ( len (f | n) = n or n < 1 or n > len f ) by FINSEQ_3:25;
then len (f | n) <= n by FINSEQ_1:58, A1, NAT_1:14;
hence (f | n) /^ n is empty by FINSEQ_5:32; :: thesis: verum

end;

suppose n = 0 ; :: thesis: (f | n) /^ n is empty

then f | n = {} ;
hence (f | n) /^ n is empty ; :: thesis: verum

end;

end;