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