reconsider i = l as Element of NAT by ORDINAL1:def 13;
l = il. i ;
hence ex b₁ being natural number st il. b₁ = l ; :: thesis: verum