now

take n = 0 ; :: thesis: for x being set st x in rng {} holds
ex t being FinSequence st
( t = x & len t = n )
let x be set ; :: thesis: ( x in rng {} implies ex t being FinSequence st
( t = x & len t = n ) )
assume x in rng {} ; :: thesis: ex t being FinSequence st
( t = x & len t = n )
hence ex t being FinSequence st
( t = x & len t = n ) ; :: thesis: verum

end;

hence {} is tabular by Def1; :: thesis: verum