let f be Function; :: thesis: ( f is Cardinal-yielding iff for y being set st y in rng f holds
y is Cardinal )

hereby :: thesis: ( ( for y being set st y in rng f holds
y is Cardinal ) implies f is Cardinal-yielding )

assume A1: f is Cardinal-yielding ; :: thesis: for y being set st y in rng f holds
y is Cardinal
let y be set ; :: thesis: ( y in rng f implies y is Cardinal )
assume y in rng f ; :: thesis: y is Cardinal
then ex x being object st
( x in dom f & y = f . x ) by FUNCT_1:def 3;
hence y is Cardinal by A1; :: thesis: verum

end;

assume A2: for y being set st y in rng f holds
y is Cardinal ; :: thesis: f is Cardinal-yielding
let x be object ; :: according to CARD_3:def 1 :: thesis: ( not x in dom f or f . x is set )
assume x in dom f ; :: thesis: f . x is set
then f . x in rng f by FUNCT_1:def 3;
hence f . x is set by A2; :: thesis: verum