set x = the Element of X;
reconsider A = {[b, the Element of X]} as array of X ;
take A ; :: thesis: ( not A is empty & A is b -based & A is finite & A is X -valued )
thus ( not A is empty & A is b -based & A is finite & A is X -valued ) ; :: thesis: verum