let ff be Cardinal-Function; :: thesis: Card ff = ff

now

let x be set ; :: thesis: ( x in dom ff implies ff . x = card (ff . x) )
assume x in dom ff ; :: thesis: ff . x = card (ff . x)
then reconsider M = ff . x as Cardinal by Def1;
card M = M by CARD_1:def 5;
hence ff . x = card (ff . x) ; :: thesis: verum

end;

hence Card ff = ff by Def2; :: thesis: verum