let a be natural number ; :: thesis: seq a,0 = {}

hereby :: thesis: verum

consider x being Element of seq a,0 ;
assume A1: seq a,0 <> {} ; :: thesis: contradiction
then reconsider x = x as Element of NAT by TARSKI:def 3;
( 1 + a <= x & x <= 0 + a ) by A1, Th1;
hence contradiction by NAT_1:13; :: thesis: verum

end;