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

now :: thesis: for x being object st x in dom ff holds
ff . x = card (ff . x)

let x be object ; :: 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 ;
hence ff . x = card (ff . x) ; :: thesis: verum

end;

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