let F be Cardinal-Function; :: thesis: for x being object st x in dom F holds
card (F . x) = F . x
let x be object ; :: thesis: ( x in dom F implies card (F . x) = F . x )
assume x in dom F ; :: thesis: card (F . x) = F . x
then reconsider M = F . x as Cardinal by Def1;
card M = M ;
hence card (F . x) = F . x ; :: thesis: verum