reconsider f = <*1*> as FinSequence of NAT ;
take f ; :: thesis: ( not f is empty & f is without_zero )
thus not f is empty ; :: thesis: f is without_zero
thus not 0 in rng f by Lm1; :: according to FREEALG:def 2 :: thesis: verum