reconsider f = <*> NAT as FinSequence of NAT ;
A1: f /^ (len f) = {} by RFINSEQ:27;

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

suppose n = 0 ; :: thesis: {} /^ n is empty

hence {} /^ n is empty by A1; :: thesis: verum

end;

suppose n > 0 ; :: thesis: {} /^ n is empty

then n > len {} ;
hence {} /^ n is empty by RFINSEQ:def 1; :: thesis: verum

end;

end;