set A = the empty array of a,X;
take the empty array of a,X ; :: thesis: ( the empty array of a,X is b -based & the empty array of a,X is natural-valued & the empty array of a,X is integer-valued & the empty array of a,X is real-valued & the empty array of a,X is complex-valued & the empty array of a,X is finite )
thus ( the empty array of a,X is b -based & the empty array of a,X is natural-valued & the empty array of a,X is integer-valued & the empty array of a,X is real-valued & the empty array of a,X is complex-valued & the empty array of a,X is finite ) by Th002; :: thesis: verum