set x = the natural number ;
reconsider A = {[b, the natural number ]} as natural-valued array ;
take A ; :: thesis: ( not A is empty & A is b -based & A is natural-valued & A is integer-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 integer-valued & A is real-valued & A is complex-valued & A is finite ) ; :: thesis: verum