consider M being Cardinal;
consider X being set ;
take f = X --> M; :: thesis: f is Cardinal-yielding
let x be set ; :: according to CARD_3:def 1 :: thesis: ( x in dom f implies f . x is Cardinal )
assume x in dom f ; :: thesis: f . x is Cardinal
hence f . x is Cardinal by FUNCOP_1:13; :: thesis: verum