Description: Alternative definition of the value of a function, ( F ''' A ) ,
also known as function application. In contrast to ( FA ) = (/)
(see df-fv and ndmfv ), ( F ''' A ) = _V if F is not defined for
A! (Contributed by Alexander van der Vekens, 25-May-2017)(Revised by BJ/AV, 25-Aug-2022)