set x = the Nat;
reconsider A = {[b, the Nat]} as natural-valued array ;
take A ; :: thesis: ( not A is empty & A is b -based & A is natural-valued & A is INT -valued & A is real-valued & A is complex-valued & A is finite )
thus ( not A is empty & A is b -based & A is natural-valued & A is INT -valued & A is real-valued & A is complex-valued & A is finite ) ; :: thesis: verum