let s be array; :: thesis: ( s = {[a,x]} implies ( s is a -based & s is succ a -limited ) )
assume A0: s = {[a,x]} ; :: thesis: ( s is a -based & s is succ a -limited )
A2: dom s = {a} by A0, FUNCT_5:12;
thus s is a -based :: thesis: s is succ a -limited

proof

let b be ordinal number ; :: according to EXCHSORT:def 2 :: thesis: ( b in proj1 s implies ( a in proj1 s & a c= b ) )
assume A1: b in proj1 s ; :: thesis: ( a in proj1 s & a c= b )
thus ( a in proj1 s & a c= b ) by A1, A2, TARSKI:def 1; :: thesis: verum

end;

sup (dom s) = succ a by A2, ORDINAL2:23;
hence s is succ a -limited by LI; :: thesis: verum