let x be set ; :: according to CARD_3:def 1 :: thesis: ( x in dom (X --> K) implies (X --> K) . x is Cardinal )
assume x in dom (X --> K) ; :: thesis: (X --> K) . x is Cardinal
hence (X --> K) . x is Cardinal by FUNCOP_1:13; :: thesis: verum