for ff being Cardinal-Function holds Card ff = ff