let p be FinSequence; :: thesis: ( p is m1 + 0 -element implies not p is empty )
assume p is m1 + 0 -element ; :: thesis: not p is empty
then len p = m1 by CARD_1:def 7;
hence not p is empty ; :: thesis: verum