let p be FinSequence; :: thesis: ( p is m + 1 -element implies not p is empty )
set M = m + 1;
assume p is m + 1 -element ; :: thesis: not p is empty
then reconsider pp = p as (m + 1) + 0 -element FinSequence ;
not pp is empty ;
hence not p is empty ; :: thesis: verum