let F be Function; :: thesis: ( F is empty implies F is finite-yielding )
assume A3: F is empty ; :: thesis: F is finite-yielding
let x be set ; :: according to CARD_FIN:def 3 :: thesis: F . x is finite
thus F . x is finite by A3; :: thesis: verum