let s be array; :: thesis: ( s = {[a,x]} implies ( s is a -based & s is succ a -limited ) )
assume A1: s = {[a,x]} ; :: thesis: ( s is a -based & s is succ a -limited )
A2: dom s = {a} by A1, FUNCT_5:12;
thus s is a -based by A2, TARSKI:def 1; :: thesis: s is succ a -limited
sup (dom s) = succ a by A2, ORDINAL2:23;
hence s is succ a -limited ; :: thesis: verum