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